From 609d744b033475238c91bfc87857263dfdbeb41f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Sat, 5 Jun 2021 00:46:07 +0200
Subject: [PATCH 1/8] Updating to Coq 8.7

---
 _CoqProject        |  1 +
 src/fAux.ml        |  6 ++++
 src/fPlugin.ml     | 72 ++++++++++++++++++++++++++++------------------
 src/fPlugin.mli    |  2 +-
 src/fTranslate.ml  | 21 +++++++-------
 src/forcing.mllib  |  1 +
 src/g_forcing.ml4  |  9 ++----
 theories/Forcing.v |  1 +
 8 files changed, 68 insertions(+), 45 deletions(-)
 create mode 100644 src/fAux.ml

diff --git a/_CoqProject b/_CoqProject
index 3778e4c..ddba329 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,6 +1,7 @@
 -R theories Forcing
 -I src
 
+src/fAux.ml
 src/fTranslate.ml
 src/fTranslate.mli
 src/fPlugin.ml
diff --git a/src/fAux.ml b/src/fAux.ml
new file mode 100644
index 0000000..9fb975a
--- /dev/null
+++ b/src/fAux.ml
@@ -0,0 +1,6 @@
+(** Utilities *)
+
+let clos_norm_flags flgs env t =
+  CClosure.norm_val
+    (CClosure.create_clos_infos flgs env)
+    (CClosure.inject t)
diff --git a/src/fPlugin.ml b/src/fPlugin.ml
index 2568b49..5761045 100644
--- a/src/fPlugin.ml
+++ b/src/fPlugin.ml
@@ -50,45 +50,51 @@ let in_translator : translator_obj -> obj =
 let empty_translator = Refmap.empty
 
 let force_tac cat c =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.nf_enter (begin fun gl ->
     let env = Proofview.Goal.env gl in
-    let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in
+    let sigma = Proofview.Goal.sigma gl in
+    let cat =
+      let (obj, hom) = cat in {
+          FTranslate.cat_obj = EConstr.to_constr sigma obj;
+          FTranslate.cat_hom = EConstr.to_constr sigma hom;
+        } in
+    let c = EConstr.to_constr sigma c in
     let (sigma, ans) = FTranslate.translate !translator cat env sigma c in
-    let sigma, _ = Typing.type_of env sigma ans in
+    let sigma, _ = Typing.type_of env sigma (EConstr.of_constr ans) in
     Proofview.Unsafe.tclEVARS sigma <*>
-    Tactics.letin_tac None Names.Name.Anonymous ans None Locusops.allHyps
-  end }
+    Tactics.letin_tac None Names.Name.Anonymous (EConstr.of_constr ans) None Locusops.allHyps
+  end)
 
 let force_solve cat c =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.nf_enter (begin fun gl ->
     let env = Proofview.Goal.env gl in
-    let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in
+    let sigma = Proofview.Goal.sigma gl in
     let (sigma, ans) = FTranslate.translate !translator cat env sigma c in
     (*     msg_info (Termops.print_constr ans); *)
-    let sigma, _ = Typing.type_of env sigma ans in
+    let sigma, _ = Typing.type_of env sigma (EConstr.of_constr ans) in
     Proofview.Unsafe.tclEVARS sigma <*>
-    Refine.refine_casted {Sigma.run =  begin fun h -> Sigma.here ans h end }
-  end }
+    Refine.refine_casted ~typecheck:false (fun sigma -> (sigma,EConstr.of_constr ans))
+  end)
 
 let force_translate_constant cat cst ids =
   let id = match ids with
   | None -> translate_name (Nametab.basename_of_global (ConstRef cst))
   | Some [id] -> id
-  | Some _ -> error "Not the right number of provided names"
+  | Some _ -> user_err (Pp.str "Not the right number of provided names")
   in
   (** Translate the type *)
   let typ = Universes.unsafe_type_of_global (ConstRef cst) in
   let env = Global.env () in
   let sigma = Evd.from_env env in
   let (sigma, typ) = FTranslate.translate_type !translator cat env sigma typ in
-  let sigma, _ = Typing.type_of env sigma typ in
+  let sigma, _ = Typing.type_of env sigma (EConstr.of_constr typ) in
   let _uctx = Evd.evar_universe_context sigma in
   (** Define the term by tactic *)
   let body = Option.get (Global.body_of_constant cst) in
   let (sigma, body) = FTranslate.translate !translator cat env sigma body in
 (*   msg_info (Termops.print_constr body); *)
   let evdref = ref sigma in
-  let () = Typing.e_check env evdref body typ in
+  let () = Typing.e_check env evdref (EConstr.of_constr body) (EConstr.of_constr typ) in
   let sigma = !evdref in
   let (_, uctx) = Evd.universe_context sigma in
   let ce = Declare.definition_entry ~types:typ ~univs:uctx body in
@@ -156,7 +162,8 @@ let force_translate_inductive cat ind ids =
       let fold (sigma, ctxt) decl =
         let (x, o, t_) = RelDecl.to_tuple decl in
         let (sigma, tr_t_) = FTranslate.translate_type translator cat env sigma t_ in
-        (sigma, RelDecl.of_tuple (x, o, tr_t_) :: ctxt)
+        assert (o = None);
+        (sigma, RelDecl.LocalAssum (x, tr_t_) :: ctxt)
       in
       let (sigma, tr_arity) = List.fold_left fold (sigma, []) oib.mind_arity_ctxt in
       let open RelDecl in
@@ -181,8 +188,11 @@ let force_translate_inductive cat ind ids =
     let (sigma, s) =
       let evdref = ref sigma in
       let s =
-        if List.mem Sorts.InType body.mind_kelim then Evarutil.e_new_Type env evdref
-        else mkProp
+        if List.mem Sorts.InType body.mind_kelim then
+          let s = Evarutil.e_new_Type env evdref in
+          EConstr.to_constr !evdref s
+        else
+          mkProp
       in
       !evdref, s
     in
@@ -212,7 +222,7 @@ let force_translate_inductive cat ind ids =
             toplevel forcing condition, which is not the case here. *)
         FTranslate.translate_type ~toplevel:false translator cat envtr sigma typ in
       let typ_ = Vars.replace_vars substfn typ_ in 
-      let typ_ = Reductionops.nf_beta Evd.empty typ_ in
+      let typ_ = FAux.clos_norm_flags CClosure.beta env typ_ in 
       let typ_ = Vars.substn_vars (List.length params + 1) invsubst typ_ in
       let envtyp_ =
         Environ.push_rel (RelDecl.LocalAssum (Name (Nameops.add_suffix body.mind_typename "_f"),
@@ -220,8 +230,8 @@ let force_translate_inductive cat ind ids =
           env
       in
       let envtyp_ = Environ.push_rel_context params envtyp_ in
-      let sigma, ty = Typing.type_of envtyp_ sigma typ_ in                             
-      let sigma, b = Reductionops.infer_conv ~pb:Reduction.CUMUL envtyp_ sigma ty s in
+      let sigma, ty = Typing.type_of envtyp_ sigma (EConstr.of_constr typ_) in
+      let sigma, b = Reductionops.infer_conv ~pb:Reduction.CUMUL envtyp_ sigma ty (EConstr.of_constr s) in
       (sigma, eta_reduce typ_ :: lc_)
     in
     let typename, consnames = match ids with
@@ -230,7 +240,7 @@ let force_translate_inductive cat ind ids =
     | Some ids when List.length ids = Array.length body.mind_consnames + 1 ->
       (List.hd ids, List.tl ids)
     | _ ->
-      error "Not the right number of provided names"
+      user_err (Pp.str "Not the right number of provided names")
     in
     let (sigma, lc_) = Array.fold_left fold_lc (sigma, []) body.mind_user_lc in
     let body_ = {
@@ -240,6 +250,8 @@ let force_translate_inductive cat ind ids =
       mind_entry_consnames = consnames;
       mind_entry_lc = List.rev lc_;
     } in
+
+
     (sigma, body_ :: bodies_)
   in
   (** We proceed to the whole mutual block *)
@@ -252,10 +264,10 @@ let force_translate_inductive cat ind ids =
   let (sigma, bodies_) = Array.fold_right (make_one_entry params_) mib.mind_packets (sigma, []) in
   let _debug b =
     let open Feedback in
-    msg_info (Nameops.pr_id b.mind_entry_typename ++ str " : " ++ Termops.print_constr (it_mkProd_or_LetIn b.mind_entry_arity params_));
+    msg_info (Nameops.pr_id b.mind_entry_typename ++ str " : " ++ Printer.pr_constr (it_mkProd_or_LetIn b.mind_entry_arity params_));
     let cs = List.combine b.mind_entry_consnames b.mind_entry_lc in
     let pr_constructor (id, tpe) =
-      msg_info (Nameops.pr_id id ++ str " : " ++ Termops.print_constr tpe)
+      msg_info (Nameops.pr_id id ++ str " : " ++ Printer.pr_constr tpe)
     in
     List.iter pr_constructor cs
   in
@@ -265,13 +277,17 @@ let force_translate_inductive cat ind ids =
     | RelDecl.LocalDef (na,b,_) -> (Nameops.out_name na, LocalDefEntry b)
   in
   let params_ = List.map make_param params_ in
-  let (_, uctx) = Evd.universe_context sigma in
+  let uctx =
+    let (_,uctx) = Evd.universe_context sigma in
+    match mib.mind_universes with
+    | Monomorphic_ind _ -> Monomorphic_ind_entry uctx
+    | Polymorphic_ind _ -> (* TODO *) Polymorphic_ind_entry uctx
+    | Cumulative_ind cu -> (* TODO *) assert false in
   let mib_ = {
     mind_entry_record = record;
     mind_entry_finite = mib.mind_finite;
     mind_entry_params = params_;
     mind_entry_inds = bodies_;
-    mind_entry_polymorphic = mib.mind_polymorphic;
     mind_entry_universes = uctx;
     mind_entry_private = mib.mind_private;
   } in
@@ -295,7 +311,7 @@ let force_translate (obj, hom) gr ids =
   let ans = match gr with
   | ConstRef cst -> force_translate_constant cat cst ids
   | IndRef ind -> force_translate_inductive cat ind ids
-  | _ -> error "Translation not handled."
+  | _ -> user_err (Pp.str "Translation not handled.")
   in
   let () = Lib.add_anonymous_leaf (in_translator ans) in
   let msg_translate (src, dst) =
@@ -323,7 +339,7 @@ let force_implement (obj, hom) id typ idopt =
   let (typ, uctx) = Constrintern.interp_type env sigma typ in
   let sigma = Evd.from_ctx uctx in
   let (sigma, typ_) = FTranslate.translate_type !translator cat env sigma typ in
-  let (sigma, _) = Typing.type_of env sigma typ_ in
+  let (sigma, _) = Typing.type_of env sigma (EConstr.of_constr typ_) in
   let hook _ dst =
     (** Declare the original term as an axiom *)
     let param = (None, false, (typ, Evd.evar_context_universe_context uctx), None) in
@@ -333,8 +349,8 @@ let force_implement (obj, hom) id typ idopt =
     Lib.add_anonymous_leaf (in_translator [ConstRef cst, dst])
   in
   let hook ctx = Lemmas.mk_hook hook in
-  let sigma, _ = Typing.type_of env sigma typ_ in
-  let () = Lemmas.start_proof_univs id_ kind sigma typ_ hook in
+  let sigma, _ = Typing.type_of env sigma (EConstr.of_constr typ_) in
+  let () = Lemmas.start_proof_univs id_ kind sigma (EConstr.of_constr typ_) hook in
   ()
 
 (** Error handling *)
diff --git a/src/fPlugin.mli b/src/fPlugin.mli
index 1893d37..41299fd 100644
--- a/src/fPlugin.mli
+++ b/src/fPlugin.mli
@@ -2,7 +2,7 @@ open Names
 open Libnames
 open Proofview
 
-val force_tac : FTranslate.category -> Constr.t -> unit tactic
+val force_tac : (EConstr.t * EConstr.t) -> EConstr.t -> unit tactic
 
 val force_translate : (reference * reference) -> reference -> Id.t list option -> unit
 
diff --git a/src/fTranslate.ml b/src/fTranslate.ml
index e75e613..7f5d7e6 100644
--- a/src/fTranslate.ml
+++ b/src/fTranslate.ml
@@ -3,10 +3,8 @@ open Term
 open Declarations
 open Environ
 open Globnames
-open Pp
 
 module RelDecl = Context.Rel.Declaration
-module NamedDecl = Context.Named.Declaration
 
 type translator = global_reference Refmap.t
 exception MissingGlobal of global_reference
@@ -238,8 +236,12 @@ let rec otranslate env fctx sigma c = match kind_of_term c with
       (** For every translated index, the corresponding variable is added
           to the forcing context *)
        let (sigma, u_) = otranslate_boxed_type env fctx sigma u in
+       let (sigma, o_) = match o with
+         | None -> (sigma, None)
+         | Some o -> let (sigma, o) = otranslate_boxed env fctx sigma o in (sigma, Some o) in
        let fctx = add_variable fctx in
-       (sigma, fctx), RelDecl.of_tuple (na, o, u_)
+       let decl = match o_ with None -> RelDecl.LocalAssum (na, u_) | Some o_ -> RelDecl.LocalDef (na, o_, u_) in
+       (sigma, fctx), decl
      in
      let (sigma, fctx), args = CList.fold_map fold (sigma, fctx) args in
      let (sigma, self_) = otranslate_type env fctx sigma self in
@@ -250,9 +252,9 @@ let rec otranslate env fctx sigma c = match kind_of_term c with
      let flags = let open CClosure in
        RedFlags.red_add betaiota RedFlags.fDELTA
      in
-     let r_ = Reductionops.clos_norm_flags flags env Evd.empty r_ in
+     let r_ = FAux.clos_norm_flags flags env r_ in
      let r_ = Vars.substnl [it_mkLambda_or_LetIn (mkVar selfid) ext] 1 (Vars.lift 1 r_) in
-     let r_ = Reductionops.nf_beta Evd.empty r_ in 
+     let r_ = FAux.clos_norm_flags CClosure.beta env r_ in
      let r_ = Vars.subst_var selfid r_ in
      let r_ = it_mkLambda_or_LetIn r_ (RelDecl.LocalAssum (na, self_) :: args) in
      (sigma, r_)       
@@ -338,14 +340,13 @@ let translate_context ?(toplevel = true) ?lift translator cat env sigma ctx =
   let empty = empty translator cat lift env in
   let fold decl (sigma, fctx, ctx_) =
     let (na, body, t) = RelDecl.to_tuple decl in
-    let (sigma, body_) = match body with
-    | None -> (sigma, None)
-    | Some _ -> assert false
-    in
     let (ext, tfctx) = extend fctx in
     let (sigma, t_) = otranslate_type env tfctx sigma t in
     let t_ = it_mkProd_or_LetIn t_ ext in
-    let decl_ = RelDecl.of_tuple (na, body_, t_) in
+    let (sigma, decl_) = match body with
+    | None -> (sigma, RelDecl.LocalAssum (na, t_))
+    | Some _ -> assert false
+    in
     let fctx = add_variable fctx in
     (sigma, fctx, decl_ :: ctx_)
   in
diff --git a/src/forcing.mllib b/src/forcing.mllib
index 59fc6cf..09a86c3 100644
--- a/src/forcing.mllib
+++ b/src/forcing.mllib
@@ -1,3 +1,4 @@
+FAux
 FTranslate
 FPlugin
 G_forcing
diff --git a/src/g_forcing.ml4 b/src/g_forcing.ml4
index 4f7cab8..b5d2e6a 100644
--- a/src/g_forcing.ml4
+++ b/src/g_forcing.ml4
@@ -1,15 +1,12 @@
-open Constrarg
+open Ltac_plugin
+open Stdarg
 open Extraargs
 
 DECLARE PLUGIN "forcing"
 
 TACTIC EXTEND force
 | [ "force" constr(obj) constr(hom) constr(c) ] -> [
-  let cat = {
-    FTranslate.cat_obj = obj;
-    FTranslate.cat_hom = hom;
-  } in
-  FPlugin.force_tac cat c
+  FPlugin.force_tac (obj,hom) c
 ]
 END
 
diff --git a/theories/Forcing.v b/theories/Forcing.v
index 10d8a1b..bddf721 100644
--- a/theories/Forcing.v
+++ b/theories/Forcing.v
@@ -1 +1,2 @@
+Declare ML Module "ltac_plugin".
 Declare ML Module "forcing".

From da02c0ba82efca6bbf0f7f3cfc8d51cbff161c33 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Sat, 5 Jun 2021 10:56:23 +0200
Subject: [PATCH 2/8] Updating to Coq 8.8

---
 src/fAux.ml       |  1 +
 src/fPlugin.ml    | 40 +++++++++++++++++++++-------------------
 src/fTranslate.ml | 13 +++++++------
 3 files changed, 29 insertions(+), 25 deletions(-)

diff --git a/src/fAux.ml b/src/fAux.ml
index 9fb975a..62f826a 100644
--- a/src/fAux.ml
+++ b/src/fAux.ml
@@ -3,4 +3,5 @@
 let clos_norm_flags flgs env t =
   CClosure.norm_val
     (CClosure.create_clos_infos flgs env)
+    (CClosure.create_tab ())
     (CClosure.inject t)
diff --git a/src/fPlugin.ml b/src/fPlugin.ml
index 5761045..0487809 100644
--- a/src/fPlugin.ml
+++ b/src/fPlugin.ml
@@ -2,7 +2,9 @@ open CErrors
 open Pp
 open Util
 open Names
+open Nameops
 open Term
+open Constr
 open Decl_kinds
 open Libobject
 open Globnames
@@ -83,20 +85,19 @@ let force_translate_constant cat cst ids =
   | Some _ -> user_err (Pp.str "Not the right number of provided names")
   in
   (** Translate the type *)
-  let typ = Universes.unsafe_type_of_global (ConstRef cst) in
   let env = Global.env () in
   let sigma = Evd.from_env env in
+  let typ, _uctx = Global.type_of_global_in_context env (ConstRef cst) in
   let (sigma, typ) = FTranslate.translate_type !translator cat env sigma typ in
   let sigma, _ = Typing.type_of env sigma (EConstr.of_constr typ) in
-  let _uctx = Evd.evar_universe_context sigma in
   (** Define the term by tactic *)
-  let body = Option.get (Global.body_of_constant cst) in
+  let body, _ = Option.get (Global.body_of_constant cst) in
   let (sigma, body) = FTranslate.translate !translator cat env sigma body in
-(*   msg_info (Termops.print_constr body); *)
+(*  Pp.pp_with Format.err_formatter (Printer.pr_constr_env env sigma body);*)
   let evdref = ref sigma in
   let () = Typing.e_check env evdref (EConstr.of_constr body) (EConstr.of_constr typ) in
   let sigma = !evdref in
-  let (_, uctx) = Evd.universe_context sigma in
+  let uctx = Evd.const_univ_entry ~poly:false sigma in
   let ce = Declare.definition_entry ~types:typ ~univs:uctx body in
   let cd = Entries.DefinitionEntry ce in
   let decl = (cd, IsProof Lemma) in
@@ -105,20 +106,20 @@ let force_translate_constant cat cst ids =
 
 let eta_reduce c =
   let rec aux c =
-    match kind_of_term c with
+    match kind c with
     | Lambda (n, t, b) ->
        let rec eta b =
-	 match kind_of_term b with
+	 match kind b with
 	 | App (f, args) ->
 	    if isRelN 1 (Array.last args) then
 	      let args', _ = Array.chop (Array.length args - 1) args in
 	      if Array.for_all (Vars.noccurn 1) args' then Vars.subst1 mkProp (mkApp (f, args'))
-	      else let b' = aux b in if Term.eq_constr b b' then c else eta b'
-	    else let b' = aux b in if Term.eq_constr b b' then c else eta b'
+	      else let b' = aux b in if Constr.equal b b' then c else eta b'
+	    else let b' = aux b in if Constr.equal b b' then c else eta b'
 	 | _ -> let b' = aux b in
-	    if Term.eq_constr b' b then c else eta b'
+	    if Constr.equal b' b then c else eta b'
        in eta b
-    | _ -> map_constr aux c
+    | _ -> Constr.map aux c
   in aux c
 
 let get_mind_globrefs mind =
@@ -264,24 +265,23 @@ let force_translate_inductive cat ind ids =
   let (sigma, bodies_) = Array.fold_right (make_one_entry params_) mib.mind_packets (sigma, []) in
   let _debug b =
     let open Feedback in
-    msg_info (Nameops.pr_id b.mind_entry_typename ++ str " : " ++ Printer.pr_constr (it_mkProd_or_LetIn b.mind_entry_arity params_));
+    msg_info (Names.Id.print b.mind_entry_typename ++ str " : " ++ Printer.pr_constr_env env sigma (it_mkProd_or_LetIn b.mind_entry_arity params_));
     let cs = List.combine b.mind_entry_consnames b.mind_entry_lc in
     let pr_constructor (id, tpe) =
-      msg_info (Nameops.pr_id id ++ str " : " ++ Printer.pr_constr tpe)
+      msg_info (Names.Id.print id ++ str " : " ++ Printer.pr_constr_env env sigma tpe)
     in
     List.iter pr_constructor cs
   in
 (*   List.iter debug bodies_; *)
   let make_param = function
-    | RelDecl.LocalAssum (na,t) -> (Nameops.out_name na, LocalAssumEntry t)
-    | RelDecl.LocalDef (na,b,_) -> (Nameops.out_name na, LocalDefEntry b)
+    | RelDecl.LocalAssum (na,t) -> (Name.get_id na, LocalAssumEntry t)
+    | RelDecl.LocalDef (na,b,_) -> (Name.get_id na, LocalDefEntry b)
   in
   let params_ = List.map make_param params_ in
   let uctx =
-    let (_,uctx) = Evd.universe_context sigma in
     match mib.mind_universes with
-    | Monomorphic_ind _ -> Monomorphic_ind_entry uctx
-    | Polymorphic_ind _ -> (* TODO *) Polymorphic_ind_entry uctx
+    | Monomorphic_ind _ -> Monomorphic_ind_entry (Evd.universe_context_set sigma)
+    | Polymorphic_ind _ -> (* TODO *) Polymorphic_ind_entry (Evd.to_universe_context sigma)
     | Cumulative_ind cu -> (* TODO *) assert false in
   let mib_ = {
     mind_entry_record = record;
@@ -338,11 +338,13 @@ let force_implement (obj, hom) id typ idopt =
   let sigma = Evd.from_env env in
   let (typ, uctx) = Constrintern.interp_type env sigma typ in
   let sigma = Evd.from_ctx uctx in
+  let typ = EConstr.to_constr sigma typ in
   let (sigma, typ_) = FTranslate.translate_type !translator cat env sigma typ in
   let (sigma, _) = Typing.type_of env sigma (EConstr.of_constr typ_) in
   let hook _ dst =
     (** Declare the original term as an axiom *)
-    let param = (None, false, (typ, Evd.evar_context_universe_context uctx), None) in
+    let uctx = Evd.universe_context_set sigma in
+    let param = (None, (typ, Entries.Monomorphic_const_entry uctx), None) in
     let cb = Entries.ParameterEntry param in
     let cst = Declare.declare_constant id (cb, IsDefinition Definition) in
     (** Attach the axiom to the forcing implementation *)
diff --git a/src/fTranslate.ml b/src/fTranslate.ml
index 7f5d7e6..877eabe 100644
--- a/src/fTranslate.ml
+++ b/src/fTranslate.ml
@@ -1,5 +1,6 @@
 open Names
 open Term
+open Constr
 open Declarations
 open Environ
 open Globnames
@@ -24,7 +25,7 @@ let knt_name = Name (Id.of_string "k")
 let hom cat a b =
   let lft = mkApp (cat.cat_hom, [| Vars.lift 1 b; mkRel 1 |]) in
   let rgt = mkApp (cat.cat_hom, [| Vars.lift 2 a; mkRel 2 |]) in
-  let arr = mkArrow lft rgt in
+  let arr = Term.mkArrow lft rgt in
   mkProd (obj_name, cat.cat_obj, arr)
 
 let refl cat a =
@@ -158,7 +159,7 @@ let apply_global env sigma gr u fctx =
 
 (** Forcing translation core *)
 
-let rec otranslate env fctx sigma c = match kind_of_term c with
+let rec otranslate env fctx sigma c = match kind c with
 | Rel n ->
   let ans = translate_var fctx n in
   (sigma, ans)
@@ -209,7 +210,7 @@ let rec otranslate env fctx sigma c = match kind_of_term c with
 | App (t, args) ->
   let (sigma, t_) = otranslate env fctx sigma t in
   let fold sigma u = otranslate_boxed env fctx sigma u in
-  let (sigma, args_) = CArray.fold_map fold sigma args in
+  let (sigma, args_) = CArray.fold_left_map fold sigma args in
   let app = mkApp (t_, args_) in
   (sigma, app)
 | Var id ->
@@ -243,7 +244,7 @@ let rec otranslate env fctx sigma c = match kind_of_term c with
        let decl = match o_ with None -> RelDecl.LocalAssum (na, u_) | Some o_ -> RelDecl.LocalDef (na, o_, u_) in
        (sigma, fctx), decl
      in
-     let (sigma, fctx), args = CList.fold_map fold (sigma, fctx) args in
+     let (sigma, fctx), args = CList.fold_left_map fold (sigma, fctx) args in
      let (sigma, self_) = otranslate_type env fctx sigma self in
      let fctx_ = add_variable fctx in
      let (sigma, r_) = otranslate_type env fctx_ sigma r_ in
@@ -261,7 +262,7 @@ let rec otranslate env fctx sigma c = match kind_of_term c with
    in
    let (sigma, r_) = fix_return_clause env fctx sigma r in
    let fold sigma u = otranslate env fctx sigma u in
-   let (sigma, p_) = CArray.fold_map fold sigma p in
+   let (sigma, p_) = CArray.fold_left_map fold sigma p in
    (sigma, mkCase (ci_, r_, c_, p_))
 | Fix f -> assert false
 | CoFix f -> assert false
@@ -273,7 +274,7 @@ and otranslate_ind env fctx sigma ind u args =
   let ind_ = get_inductive fctx ind in
   let (_, oib) = Inductive.lookup_mind_specif env ind_ in
   let fold sigma u = otranslate_boxed env fctx sigma u in
-  let (sigma, args_) = CArray.fold_map fold sigma args in
+  let (sigma, args_) = CArray.fold_left_map fold sigma args in
   (** First parameter is the toplevel forcing condition *)
   let _, paramtyp = CList.sep_last oib.mind_arity_ctxt in
   let nparams = List.length paramtyp in

From f67fb15e818d3f9a883d3738800b88644c3217eb Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Sat, 5 Jun 2021 11:24:16 +0200
Subject: [PATCH 3/8] Updating to Coq 8.9

---
 src/fPlugin.ml     | 38 +++++++++++++++++---------------------
 src/fPlugin.mli    |  4 ++--
 src/fTranslate.ml  |  5 +++--
 src/fTranslate.mli |  8 ++++----
 4 files changed, 26 insertions(+), 29 deletions(-)

diff --git a/src/fPlugin.ml b/src/fPlugin.ml
index 0487809..231920d 100644
--- a/src/fPlugin.ml
+++ b/src/fPlugin.ml
@@ -24,7 +24,7 @@ let translate_name id =
 let translator : FTranslate.translator ref =
   Summary.ref ~name:"Forcing Global Table" Refmap.empty
 
-type translator_obj = (global_reference * global_reference) list
+type translator_obj = (GlobRef.t * GlobRef.t) list
 
 let add_translator translator l =
   List.fold_left (fun accu (src, dst) -> Refmap.add src dst accu) translator l
@@ -94,9 +94,7 @@ let force_translate_constant cat cst ids =
   let body, _ = Option.get (Global.body_of_constant cst) in
   let (sigma, body) = FTranslate.translate !translator cat env sigma body in
 (*  Pp.pp_with Format.err_formatter (Printer.pr_constr_env env sigma body);*)
-  let evdref = ref sigma in
-  let () = Typing.e_check env evdref (EConstr.of_constr body) (EConstr.of_constr typ) in
-  let sigma = !evdref in
+  let sigma = Typing.check env sigma (EConstr.of_constr body) (EConstr.of_constr typ) in
   let uctx = Evd.const_univ_entry ~poly:false sigma in
   let ce = Declare.definition_entry ~types:typ ~univs:uctx body in
   let cd = Entries.DefinitionEntry ce in
@@ -187,15 +185,11 @@ let force_translate_inductive cat ind ids =
     in
     (** Heuristic for the return type. Can we do better? *)
     let (sigma, s) =
-      let evdref = ref sigma in
-      let s =
-        if List.mem Sorts.InType body.mind_kelim then
-          let s = Evarutil.e_new_Type env evdref in
-          EConstr.to_constr !evdref s
-        else
-          mkProp
-      in
-      !evdref, s
+      if List.mem Sorts.InType body.mind_kelim then
+        let sigma, s = Evarutil.new_Type sigma in
+        (sigma, EConstr.to_constr sigma s)
+      else
+        (sigma, mkProp)
     in
     let (sigma, arity) =
       (** On obtient l'arité de l'inductif en traduisant le type de chaque indice
@@ -232,7 +226,9 @@ let force_translate_inductive cat ind ids =
       in
       let envtyp_ = Environ.push_rel_context params envtyp_ in
       let sigma, ty = Typing.type_of envtyp_ sigma (EConstr.of_constr typ_) in
-      let sigma, b = Reductionops.infer_conv ~pb:Reduction.CUMUL envtyp_ sigma ty (EConstr.of_constr s) in
+      let sigma = match Reductionops.infer_conv ~pb:Reduction.CUMUL envtyp_ sigma ty (EConstr.of_constr s) with
+        | None -> assert false 
+        | Some sigma -> sigma in
       (sigma, eta_reduce typ_ :: lc_)
     in
     let typename, consnames = match ids with
@@ -257,9 +253,9 @@ let force_translate_inductive cat ind ids =
   in
   (** We proceed to the whole mutual block *)
   let record = match mib.mind_record with
-  | None -> None
-  | Some None -> Some None
-  | Some (Some (id, _, _)) -> Some (Some (translate_name id))
+  | NotRecord -> None
+  | FakeRecord -> Some None
+  | PrimRecord info -> Some (Some (Array.map pi1 info))
   in
   let (sigma, params_) = FTranslate.translate_context translator cat env sigma mib.mind_params_ctxt in
   let (sigma, bodies_) = Array.fold_right (make_one_entry params_) mib.mind_packets (sigma, []) in
@@ -302,8 +298,8 @@ let force_translate_inductive cat ind ids =
 
 let force_translate (obj, hom) gr ids =
   let gr = Nametab.global gr in
-  let obj = Universes.constr_of_global (Nametab.global obj) in
-  let hom = Universes.constr_of_global (Nametab.global hom) in
+  let obj = UnivGen.constr_of_global (Nametab.global obj) in
+  let hom = UnivGen.constr_of_global (Nametab.global hom) in
   let cat = {
     FTranslate.cat_obj = obj;
     FTranslate.cat_hom = hom;
@@ -324,8 +320,8 @@ let force_translate (obj, hom) gr ids =
 
 let force_implement (obj, hom) id typ idopt =
   let env = Global.env () in
-  let obj = Universes.constr_of_global (Nametab.global obj) in
-  let hom = Universes.constr_of_global (Nametab.global hom) in
+  let obj = UnivGen.constr_of_global (Nametab.global obj) in
+  let hom = UnivGen.constr_of_global (Nametab.global hom) in
   let cat = {
     FTranslate.cat_obj = obj;
     FTranslate.cat_hom = hom;
diff --git a/src/fPlugin.mli b/src/fPlugin.mli
index 41299fd..cad1880 100644
--- a/src/fPlugin.mli
+++ b/src/fPlugin.mli
@@ -4,6 +4,6 @@ open Proofview
 
 val force_tac : (EConstr.t * EConstr.t) -> EConstr.t -> unit tactic
 
-val force_translate : (reference * reference) -> reference -> Id.t list option -> unit
+val force_translate : (qualid * qualid) -> qualid -> Id.t list option -> unit
 
-val force_implement : (reference * reference) -> Id.t -> Constrexpr.constr_expr -> Id.t option -> unit
+val force_implement : (qualid * qualid) -> Id.t -> Constrexpr.constr_expr -> Id.t option -> unit
diff --git a/src/fTranslate.ml b/src/fTranslate.ml
index 877eabe..e6c08ba 100644
--- a/src/fTranslate.ml
+++ b/src/fTranslate.ml
@@ -7,8 +7,8 @@ open Globnames
 
 module RelDecl = Context.Rel.Declaration
 
-type translator = global_reference Refmap.t
-exception MissingGlobal of global_reference
+type translator = GlobRef.t Refmap.t
+exception MissingGlobal of GlobRef.t
 
 (** Yoneda embedding *)
 
@@ -152,6 +152,7 @@ let apply_global env sigma gr u fctx =
     with Not_found -> raise (MissingGlobal gr)
   in
   let (sigma, c) = Evd.fresh_global env sigma p' in
+  let c = EConstr.to_constr sigma c in
   let last = last_condition fctx in
   match gr with
   | IndRef _ -> assert false
diff --git a/src/fTranslate.mli b/src/fTranslate.mli
index 700456e..21f39cb 100644
--- a/src/fTranslate.mli
+++ b/src/fTranslate.mli
@@ -7,11 +7,11 @@ type category = {
   (** Morphisms. Must be a closed term of type [cat_obj -> cat_obj -> Type]. *)
 }
 
-exception MissingGlobal of global_reference
+exception MissingGlobal of Names.GlobRef.t
 
-type translator = global_reference Refmap.t
+type translator = Names.GlobRef.t Refmap.t
 
-val hom : category -> Constr.constr -> Constr.constr -> Term.types
+val hom : category -> Constr.constr -> Constr.constr -> Constr.types
 
 val translate : ?toplevel:bool ->  ?lift:int -> translator -> category ->
   Environ.env -> Evd.evar_map -> Constr.t -> Evd.evar_map * Constr.t
@@ -20,4 +20,4 @@ val translate_type : ?toplevel:bool -> ?lift:int -> translator -> category ->
   Environ.env -> Evd.evar_map -> Constr.t -> Evd.evar_map * Constr.t
 
 val translate_context : ?toplevel:bool -> ?lift:int -> translator -> category ->
-  Environ.env -> Evd.evar_map -> Context.Rel.t -> Evd.evar_map * Context.Rel.t
+  Environ.env -> Evd.evar_map -> Constr.rel_context -> Evd.evar_map * Constr.rel_context

From 8fff975ddf8e8cf18d41d61e4dfd9660d4713e08 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Sat, 5 Jun 2021 12:56:41 +0200
Subject: [PATCH 4/8] Updating to Coq 8.10

---
 _CoqProject        |   2 +-
 src/fPlugin.ml     | 104 ++++++++++++++++++++-------------------------
 src/fPlugin.mli    |   2 +-
 src/fTranslate.ml  |  42 +++++++++---------
 src/fTranslate.mli |   6 +--
 src/g_forcing.ml4  |  27 ------------
 src/g_forcing.mlg  |  34 +++++++++++++++
 theories/Forcing.v |   4 ++
 8 files changed, 109 insertions(+), 112 deletions(-)
 delete mode 100644 src/g_forcing.ml4
 create mode 100644 src/g_forcing.mlg

diff --git a/_CoqProject b/_CoqProject
index ddba329..3a3718d 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -6,7 +6,7 @@ src/fTranslate.ml
 src/fTranslate.mli
 src/fPlugin.ml
 src/fPlugin.mli
-src/g_forcing.ml4
+src/g_forcing.mlg
 src/forcing.mllib
 
 theories/Forcing.v
diff --git a/src/fPlugin.ml b/src/fPlugin.ml
index 231920d..18d3eb9 100644
--- a/src/fPlugin.ml
+++ b/src/fPlugin.ml
@@ -2,7 +2,6 @@ open CErrors
 open Pp
 open Util
 open Names
-open Nameops
 open Term
 open Constr
 open Decl_kinds
@@ -22,21 +21,18 @@ let translate_name id =
 (** Record of translation between globals *)
 
 let translator : FTranslate.translator ref =
-  Summary.ref ~name:"Forcing Global Table" Refmap.empty
+  Summary.ref ~name:"Forcing Global Table" GlobRef.Map.empty
 
 type translator_obj = (GlobRef.t * GlobRef.t) list
 
 let add_translator translator l =
-  List.fold_left (fun accu (src, dst) -> Refmap.add src dst accu) translator l
+  List.fold_left (fun accu (src, dst) -> GlobRef.Map.add src dst accu) translator l
 							    
 let cache_translator (_, l) =
   translator := add_translator !translator l
 
 let load_translator _ l = cache_translator l
 let open_translator _ l = cache_translator l
-let subst_translator (subst, l) =
-  let map (src, dst) = (subst_global_reference subst src, subst_global_reference subst dst) in
-  List.map map l
 
 let in_translator : translator_obj -> obj =
   declare_object { (default_object "FORCING TRANSLATOR") with
@@ -49,10 +45,8 @@ let in_translator : translator_obj -> obj =
 
 (** Tactic *)
 
-let empty_translator = Refmap.empty
-
 let force_tac cat c =
-  Proofview.Goal.nf_enter (begin fun gl ->
+  Proofview.Goal.enter (begin fun gl ->
     let env = Proofview.Goal.env gl in
     let sigma = Proofview.Goal.sigma gl in
     let cat =
@@ -67,16 +61,18 @@ let force_tac cat c =
     Tactics.letin_tac None Names.Name.Anonymous (EConstr.of_constr ans) None Locusops.allHyps
   end)
 
+(*
 let force_solve cat c =
-  Proofview.Goal.nf_enter (begin fun gl ->
+  Proofview.Goal.enter (begin fun gl ->
     let env = Proofview.Goal.env gl in
     let sigma = Proofview.Goal.sigma gl in
     let (sigma, ans) = FTranslate.translate !translator cat env sigma c in
     (*     msg_info (Termops.print_constr ans); *)
     let sigma, _ = Typing.type_of env sigma (EConstr.of_constr ans) in
     Proofview.Unsafe.tclEVARS sigma <*>
-    Refine.refine_casted ~typecheck:false (fun sigma -> (sigma,EConstr.of_constr ans))
+    FAux.refine_casted ~typecheck:false (fun sigma -> (sigma,EConstr.of_constr ans))
   end)
+*)
 
 let force_translate_constant cat cst ids =
   let id = match ids with
@@ -84,18 +80,18 @@ let force_translate_constant cat cst ids =
   | Some [id] -> id
   | Some _ -> user_err (Pp.str "Not the right number of provided names")
   in
-  (** Translate the type *)
+  (* Translate the type *)
   let env = Global.env () in
   let sigma = Evd.from_env env in
-  let typ, _uctx = Global.type_of_global_in_context env (ConstRef cst) in
+  let typ, _uctx = Typeops.type_of_global_in_context env (ConstRef cst) in
   let (sigma, typ) = FTranslate.translate_type !translator cat env sigma typ in
   let sigma, _ = Typing.type_of env sigma (EConstr.of_constr typ) in
-  (** Define the term by tactic *)
+  (* Define the term by tactic *)
   let body, _ = Option.get (Global.body_of_constant cst) in
   let (sigma, body) = FTranslate.translate !translator cat env sigma body in
 (*  Pp.pp_with Format.err_formatter (Printer.pr_constr_env env sigma body);*)
   let sigma = Typing.check env sigma (EConstr.of_constr body) (EConstr.of_constr typ) in
-  let uctx = Evd.const_univ_entry ~poly:false sigma in
+  let uctx = Evd.univ_entry ~poly:false sigma in
   let ce = Declare.definition_entry ~types:typ ~univs:uctx body in
   let cd = Entries.DefinitionEntry ce in
   let decl = (cd, IsProof Lemma) in
@@ -132,25 +128,25 @@ let get_mind_globrefs mind =
   List.flatten l
 
 let force_translate_inductive cat ind ids =
-  (** From a kernel inductive body construct an entry for the inductive. There
-      are slight mismatches in the representation, in particular in the handling
-      of contexts. See {!Declarations} and {!Entries}. *)
+  (* From a kernel inductive body construct an entry for the inductive. There
+     are slight mismatches in the representation, in particular in the handling
+     of contexts. See {!Declarations} and {!Entries}. *)
   let open Declarations in
   let open Entries in
   let env = Global.env () in
   let (mib, _) = Global.lookup_inductive ind in
   let nparams = List.length mib.mind_params_ctxt in
-  (** For each block in the inductive we build the translation *)
+  (* For each block in the inductive we build the translation *)
   let substind =
     Array.map_to_list (fun oib ->
-        NamedDecl.LocalAssum (oib.mind_typename,
+        NamedDecl.LocalAssum (Context.annotR oib.mind_typename,
 			      Inductive.type_of_inductive env ((mib, oib), Univ.Instance.empty)))
       mib.mind_packets
   in
   let invsubst = List.map NamedDecl.get_id substind in
   let translator = add_translator !translator (List.map (fun id -> VarRef id, VarRef id) invsubst) in
-(** À chaque inductif I on associe une fonction λp.λparams.λindices.λ(qα), 
-    (mkVar I) p params indices *)
+  (* À chaque inductif I on associe une fonction λp.λparams.λindices.λ(qα), 
+     (mkVar I) p params indices *)
   let sigma = Evd.from_env env in
   let (sigma, substfn) = 
     let fn_oib oib = 
@@ -167,10 +163,10 @@ let force_translate_inductive cat ind ids =
       let (sigma, tr_arity) = List.fold_left fold (sigma, []) oib.mind_arity_ctxt in
       let open RelDecl in
       (sigma, it_mkLambda_or_LetIn fnbody
-         ([LocalAssum (Anonymous, FTranslate.hom cat (mkRel 3) (mkRel (3 + narityctxt)));
-           LocalAssum (Anonymous, obj)]
+         ([LocalAssum (Context.anonR, FTranslate.hom cat (mkRel 3) (mkRel (3 + narityctxt)));
+           LocalAssum (Context.anonR, obj)]
           @ tr_arity
-          @ [LocalAssum (Anonymous, obj)]))
+          @ [LocalAssum (Context.anonR, obj)]))
     in
     let fold (sigma, acc) oib =
       let (sigma, fn) = fn_oib oib in
@@ -183,7 +179,7 @@ let force_translate_inductive cat ind ids =
     | RegularArity _ -> false
     | TemplateArity _ -> true
     in
-    (** Heuristic for the return type. Can we do better? *)
+    (* Heuristic for the return type. Can we do better? *)
     let (sigma, s) =
       if List.mem Sorts.InType body.mind_kelim then
         let sigma, s = Evarutil.new_Type sigma in
@@ -192,35 +188,35 @@ let force_translate_inductive cat ind ids =
         (sigma, mkProp)
     in
     let (sigma, arity) =
-      (** On obtient l'arité de l'inductif en traduisant le type de chaque indice
-          i.e : si I ... : (i1 : A1),...,(in : An),s alors l'arité traduite 
-          est (i1 : [A1])...(in : [An]), s *)
+      (* On obtient l'arité de l'inductif en traduisant le type de chaque indice
+         i.e : si I ... : (i1 : A1),...,(in : An),s alors l'arité traduite 
+         est (i1 : [A1])...(in : [An]), s *)
       let nindexes = List.length body.mind_arity_ctxt - nparams in
       let ctx = List.firstn nindexes body.mind_arity_ctxt in
       let env' = Environ.push_rel_context mib.mind_params_ctxt env in
       let a = it_mkProd_or_LetIn s ctx in
       let (sigma, a) = FTranslate.translate_type ~toplevel:false translator cat env' sigma a in
-      (** En traduisant le type, le codomaine a aussi été traduit. On le remplace par le codomaine
-          originel *)
+      (* En traduisant le type, le codomaine a aussi été traduit. On le remplace par le codomaine
+         originel *)
       let (a, _) = decompose_prod_n nindexes a in 
       (sigma, compose_prod a s)
     in
     let fold_lc (sigma, lc_) typ =
-      (** We exploit the fact that the translation actually does not depend on
-          the rel_context of the environment except for its length. *)
+      (* We exploit the fact that the translation actually does not depend on
+         the rel_context of the environment except for its length. *)
       let env' = Environ.push_named_context substind env in
       let envtr = Environ.push_rel_context (CList.tl params) env' in
       let _, typ = decompose_prod_n nparams typ in
       let typ = Vars.substnl (List.map mkVar invsubst) nparams typ in
       let (sigma, typ_) =
-        (** The translation assumes that the first introduced variable is the
-            toplevel forcing condition, which is not the case here. *)
+        (* The translation assumes that the first introduced variable is the
+           toplevel forcing condition, which is not the case here. *)
         FTranslate.translate_type ~toplevel:false translator cat envtr sigma typ in
       let typ_ = Vars.replace_vars substfn typ_ in 
       let typ_ = FAux.clos_norm_flags CClosure.beta env typ_ in 
       let typ_ = Vars.substn_vars (List.length params + 1) invsubst typ_ in
       let envtyp_ =
-        Environ.push_rel (RelDecl.LocalAssum (Name (Nameops.add_suffix body.mind_typename "_f"),
+        Environ.push_rel (RelDecl.LocalAssum (Context.nameR (Nameops.add_suffix body.mind_typename "_f"),
 		                              it_mkProd_or_LetIn arity params))
           env
       in
@@ -251,11 +247,11 @@ let force_translate_inductive cat ind ids =
 
     (sigma, body_ :: bodies_)
   in
-  (** We proceed to the whole mutual block *)
+  (* We proceed to the whole mutual block *)
   let record = match mib.mind_record with
   | NotRecord -> None
   | FakeRecord -> Some None
-  | PrimRecord info -> Some (Some (Array.map pi1 info))
+  | PrimRecord info -> Some (Some (Array.map (fun (id,_,_,_) -> id) info))
   in
   let (sigma, params_) = FTranslate.translate_context translator cat env sigma mib.mind_params_ctxt in
   let (sigma, bodies_) = Array.fold_right (make_one_entry params_) mib.mind_packets (sigma, []) in
@@ -269,22 +265,17 @@ let force_translate_inductive cat ind ids =
     List.iter pr_constructor cs
   in
 (*   List.iter debug bodies_; *)
-  let make_param = function
-    | RelDecl.LocalAssum (na,t) -> (Name.get_id na, LocalAssumEntry t)
-    | RelDecl.LocalDef (na,b,_) -> (Name.get_id na, LocalDefEntry b)
-  in
-  let params_ = List.map make_param params_ in
   let uctx =
     match mib.mind_universes with
-    | Monomorphic_ind _ -> Monomorphic_ind_entry (Evd.universe_context_set sigma)
-    | Polymorphic_ind _ -> (* TODO *) Polymorphic_ind_entry (Evd.to_universe_context sigma)
-    | Cumulative_ind cu -> (* TODO *) assert false in
+    | Monomorphic _ -> Monomorphic_entry (Evd.universe_context_set sigma)
+    | Polymorphic _ -> Evd.univ_entry ~poly:true sigma in
   let mib_ = {
     mind_entry_record = record;
     mind_entry_finite = mib.mind_finite;
     mind_entry_params = params_;
     mind_entry_inds = bodies_;
     mind_entry_universes = uctx;
+    mind_entry_variance = mib.mind_variance;
     mind_entry_private = mib.mind_private;
   } in
   let (_, kn), _ = Declare.declare_mind mib_ in
@@ -298,8 +289,8 @@ let force_translate_inductive cat ind ids =
 
 let force_translate (obj, hom) gr ids =
   let gr = Nametab.global gr in
-  let obj = UnivGen.constr_of_global (Nametab.global obj) in
-  let hom = UnivGen.constr_of_global (Nametab.global hom) in
+  let obj = UnivGen.constr_of_monomorphic_global (Nametab.global obj) in
+  let hom = UnivGen.constr_of_monomorphic_global (Nametab.global hom) in
   let cat = {
     FTranslate.cat_obj = obj;
     FTranslate.cat_hom = hom;
@@ -320,8 +311,8 @@ let force_translate (obj, hom) gr ids =
 
 let force_implement (obj, hom) id typ idopt =
   let env = Global.env () in
-  let obj = UnivGen.constr_of_global (Nametab.global obj) in
-  let hom = UnivGen.constr_of_global (Nametab.global hom) in
+  let obj = UnivGen.constr_of_monomorphic_global (Nametab.global obj) in
+  let hom = UnivGen.constr_of_monomorphic_global (Nametab.global hom) in
   let cat = {
     FTranslate.cat_obj = obj;
     FTranslate.cat_hom = hom;
@@ -337,19 +328,18 @@ let force_implement (obj, hom) id typ idopt =
   let typ = EConstr.to_constr sigma typ in
   let (sigma, typ_) = FTranslate.translate_type !translator cat env sigma typ in
   let (sigma, _) = Typing.type_of env sigma (EConstr.of_constr typ_) in
-  let hook _ dst =
-    (** Declare the original term as an axiom *)
+  let hook _ _ _ dst =
+    (* Declare the original term as an axiom *)
     let uctx = Evd.universe_context_set sigma in
-    let param = (None, (typ, Entries.Monomorphic_const_entry uctx), None) in
+    let param = (None, (typ, Entries.Monomorphic_entry uctx), None) in
     let cb = Entries.ParameterEntry param in
     let cst = Declare.declare_constant id (cb, IsDefinition Definition) in
-    (** Attach the axiom to the forcing implementation *)
+    (* Attach the axiom to the forcing implementation *)
     Lib.add_anonymous_leaf (in_translator [ConstRef cst, dst])
   in
-  let hook ctx = Lemmas.mk_hook hook in
+  let hook = Lemmas.mk_hook hook in
   let sigma, _ = Typing.type_of env sigma (EConstr.of_constr typ_) in
-  let () = Lemmas.start_proof_univs id_ kind sigma (EConstr.of_constr typ_) hook in
-  ()
+  Lemmas.start_proof ~ontop:None id_ kind sigma (EConstr.of_constr typ_) ~hook
 
 (** Error handling *)
 
diff --git a/src/fPlugin.mli b/src/fPlugin.mli
index cad1880..2b95ae0 100644
--- a/src/fPlugin.mli
+++ b/src/fPlugin.mli
@@ -6,4 +6,4 @@ val force_tac : (EConstr.t * EConstr.t) -> EConstr.t -> unit tactic
 
 val force_translate : (qualid * qualid) -> qualid -> Id.t list option -> unit
 
-val force_implement : (qualid * qualid) -> Id.t -> Constrexpr.constr_expr -> Id.t option -> unit
+val force_implement : (qualid * qualid) -> Id.t -> Constrexpr.constr_expr -> Id.t option -> Proof_global.t
diff --git a/src/fTranslate.ml b/src/fTranslate.ml
index e6c08ba..ac3ec0a 100644
--- a/src/fTranslate.ml
+++ b/src/fTranslate.ml
@@ -7,7 +7,7 @@ open Globnames
 
 module RelDecl = Context.Rel.Declaration
 
-type translator = GlobRef.t Refmap.t
+type translator = GlobRef.t GlobRef.Map.t
 exception MissingGlobal of GlobRef.t
 
 (** Yoneda embedding *)
@@ -19,13 +19,13 @@ type category = {
   (** Morphisms. Must be of type [cat_obj -> cat_obj -> Type]. *)
 }
 
-let obj_name = Name (Id.of_string "R")
-let knt_name = Name (Id.of_string "k")
+let obj_name = Context.nameR (Id.of_string "R")
+let knt_name = Context.nameR (Id.of_string "k")
 
 let hom cat a b =
   let lft = mkApp (cat.cat_hom, [| Vars.lift 1 b; mkRel 1 |]) in
   let rgt = mkApp (cat.cat_hom, [| Vars.lift 2 a; mkRel 2 |]) in
-  let arr = Term.mkArrow lft rgt in
+  let arr = Term.mkArrow lft Sorts.Relevant rgt in
   mkProd (obj_name, cat.cat_obj, arr)
 
 let refl cat a =
@@ -70,8 +70,8 @@ type forcing_context = {
 
 (** We assume that there is a hidden topmost variable [p : Obj] in the context *)
 
-let pos_name = Name (Id.of_string "p")
-let hom_name = Name (Id.of_string "α")
+let pos_name = Context.nameR (Id.of_string "p")
+let hom_name = Context.nameR (Id.of_string "α")
 
 let dummy = mkProp
 
@@ -130,15 +130,10 @@ let translate_var fctx n =
   let m = get_var_shift n fctx in
   mkApp (mkRel m, [| p; f |])
 
-let rec untranslate_rel n c = match Constr.kind c with
-| App (t, args) when isRel t && Array.length args >= 2 ->
-  c
-| _ -> Constr.map_with_binders succ untranslate_rel n c
-
 let get_inductive fctx ind =
   let gr = IndRef ind in
   let gr_ =
-    try Refmap.find gr fctx.translator
+    try GlobRef.Map.find gr fctx.translator
     with Not_found -> raise (MissingGlobal gr)
   in
   match gr_ with
@@ -146,9 +141,9 @@ let get_inductive fctx ind =
   | _ -> assert false
 
 let apply_global env sigma gr u fctx =
-  (** FIXME *)
+  (* FIXME *)
   let p' =
-    try Refmap.find gr fctx.translator
+    try GlobRef.Map.find gr fctx.translator
     with Not_found -> raise (MissingGlobal gr)
   in
   let (sigma, c) = Evd.fresh_global env sigma p' in
@@ -182,19 +177,19 @@ let rec otranslate env fctx sigma c = match kind c with
   (sigma, ans)
 | Prod (na, t, u) ->
   let (ext0, fctx) = extend fctx in
-  (** Translation of t *)
+  (* Translation of t *)
   let (sigma, t_) = otranslate_boxed_type env fctx sigma t in
-  (** Translation of u *)
+  (* Translation of u *)
   let ufctx = add_variable fctx in
   let (sigma, u_) = otranslate_type env ufctx sigma u in
-  (** Result *)
+  (* Result *)
   let ans = mkProd (na, t_, u_) in
   let lam = it_mkLambda_or_LetIn ans ext0 in
   (sigma, lam)
 | Lambda (na, t, u) ->
-  (** Translation of t *)
+  (* Translation of t *)
   let (sigma, t_) = otranslate_boxed_type env fctx sigma t in
-  (** Translation of u *)
+  (* Translation of u *)
   let ufctx = add_variable fctx in
   let (sigma, u_) = otranslate env ufctx sigma u in
   let ans = mkLambda (na, t_, u_) in
@@ -224,10 +219,10 @@ let rec otranslate env fctx sigma c = match kind c with
   apply_global env sigma (ConstructRef c) u fctx
 | Case (ci, r, c, p) ->
    let ind_ = get_inductive fctx ci.ci_ind in
-   let ci_ = Inductiveops.make_case_info env ind_ ci.ci_pp_info.style in
+   let ci_ = Inductiveops.make_case_info env ind_ Sorts.Relevant ci.ci_pp_info.style in
    let (sigma, c_) = otranslate env fctx sigma c in
    let fix_return_clause env fctx sigma r =
-     (** The return clause structure is fun indexes self => Q
+     (* The return clause structure is fun indexes self => Q
          All indices must be boxed, but self only needs to be translated *)
      let (args, r_) = decompose_lam_assum r in
      let (na, self, args) = match args with
@@ -235,7 +230,7 @@ let rec otranslate env fctx sigma c = match kind c with
        | _ -> assert false in
      let fold (sigma, fctx) decl =
        let (na, o, u) = RelDecl.to_tuple decl in
-      (** For every translated index, the corresponding variable is added
+      (* For every translated index, the corresponding variable is added
           to the forcing context *)
        let (sigma, u_) = otranslate_boxed_type env fctx sigma u in
        let (sigma, o_) = match o with
@@ -270,13 +265,14 @@ let rec otranslate env fctx sigma c = match kind c with
 | Proj (p, c) -> assert false
 | Meta _ -> assert false
 | Evar _ -> assert false
+| Int _ -> assert false
 
 and otranslate_ind env fctx sigma ind u args =
   let ind_ = get_inductive fctx ind in
   let (_, oib) = Inductive.lookup_mind_specif env ind_ in
   let fold sigma u = otranslate_boxed env fctx sigma u in
   let (sigma, args_) = CArray.fold_left_map fold sigma args in
-  (** First parameter is the toplevel forcing condition *)
+  (* First parameter is the toplevel forcing condition *)
   let _, paramtyp = CList.sep_last oib.mind_arity_ctxt in
   let nparams = List.length paramtyp in
   let last = last_condition fctx in
diff --git a/src/fTranslate.mli b/src/fTranslate.mli
index 21f39cb..af71a77 100644
--- a/src/fTranslate.mli
+++ b/src/fTranslate.mli
@@ -1,4 +1,4 @@
-open Globnames
+open Names
 
 type category = {
   cat_obj : Constr.t;
@@ -7,9 +7,9 @@ type category = {
   (** Morphisms. Must be a closed term of type [cat_obj -> cat_obj -> Type]. *)
 }
 
-exception MissingGlobal of Names.GlobRef.t
+exception MissingGlobal of GlobRef.t
 
-type translator = Names.GlobRef.t Refmap.t
+type translator = GlobRef.t GlobRef.Map.t
 
 val hom : category -> Constr.constr -> Constr.constr -> Constr.types
 
diff --git a/src/g_forcing.ml4 b/src/g_forcing.ml4
deleted file mode 100644
index b5d2e6a..0000000
--- a/src/g_forcing.ml4
+++ /dev/null
@@ -1,27 +0,0 @@
-open Ltac_plugin
-open Stdarg
-open Extraargs
-
-DECLARE PLUGIN "forcing"
-
-TACTIC EXTEND force
-| [ "force" constr(obj) constr(hom) constr(c) ] -> [
-  FPlugin.force_tac (obj,hom) c
-]
-END
-
-VERNAC COMMAND EXTEND ForcingTranslation CLASSIFIED AS SIDEFF
-| [ "Forcing" "Translate" global(gr) "using" global(obj) global(hom) ] ->
-  [ FPlugin.force_translate (obj, hom) gr None ]
-| [ "Forcing" "Translate" global(gr) "as" ne_ident_list(id) "using" global(obj) global(hom) ] ->
-  [ FPlugin.force_translate (obj, hom) gr (Some id) ]
-END
-
-let classify_impl _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]), VtLater)
-
-VERNAC COMMAND EXTEND ForcingImplementation CLASSIFIED BY classify_impl
-| [ "Forcing" "Definition" ident(id) ":" lconstr(typ) "using" global(obj) global(hom) ] ->
-  [ FPlugin.force_implement (obj, hom) id typ None ]
-| [ "Forcing" "Definition" ident(id) ":" lconstr(typ) "as" ident(id') "using" global(obj) global(hom) ] ->
-  [ FPlugin.force_implement (obj, hom) id typ (Some id') ]
-END
diff --git a/src/g_forcing.mlg b/src/g_forcing.mlg
new file mode 100644
index 0000000..1e35f35
--- /dev/null
+++ b/src/g_forcing.mlg
@@ -0,0 +1,34 @@
+{
+
+open Ltac_plugin
+open Stdarg
+open Extraargs
+
+}
+
+DECLARE PLUGIN "forcing"
+
+TACTIC EXTEND force
+| [ "force" constr(obj) constr(hom) constr(c) ] ->
+  { FPlugin.force_tac (obj,hom) c }
+END
+
+VERNAC COMMAND EXTEND ForcingTranslation CLASSIFIED AS SIDEFF
+| [ "Forcing" "Translate" global(gr) "using" global(obj) global(hom) ] ->
+  { FPlugin.force_translate (obj, hom) gr None }
+| [ "Forcing" "Translate" global(gr) "as" ne_ident_list(id) "using" global(obj) global(hom) ] ->
+  { FPlugin.force_translate (obj, hom) gr (Some id) }
+END
+
+{
+
+let classify_impl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]), VtLater)
+
+}
+
+VERNAC COMMAND EXTEND ForcingImplementation CLASSIFIED BY { classify_impl }
+| ![ proof ] [ "Forcing" "Definition" ident(id) ":" lconstr(typ) "using" global(obj) global(hom) ] ->
+  { fun ~pstate -> Some (FPlugin.force_implement (obj, hom) id typ None) }
+| ![ proof ] [ "Forcing" "Definition" ident(id) ":" lconstr(typ) "as" ident(id') "using" global(obj) global(hom) ] ->
+  { fun ~pstate -> Some (FPlugin.force_implement (obj, hom) id typ (Some id')) }
+END
diff --git a/theories/Forcing.v b/theories/Forcing.v
index bddf721..8ee4584 100644
--- a/theories/Forcing.v
+++ b/theories/Forcing.v
@@ -1,2 +1,6 @@
 Declare ML Module "ltac_plugin".
 Declare ML Module "forcing".
+
+(* The plugin is not able to preserve the relation between parameters
+   and conclusions of an inductive type *)
+Global Unset Template Check.

From fbd72745c8b3a58cef8639591bdef3edda1c373b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Sat, 5 Jun 2021 15:18:04 +0200
Subject: [PATCH 5/8] Updating to Coq 8.11

---
 src/fPlugin.ml     | 60 ++++++++++++++++++++++------------------------
 src/fPlugin.mli    |  2 +-
 src/fTranslate.ml  | 14 +++++------
 src/g_forcing.mlg  | 12 +++++-----
 theories/Forcing.v |  4 ----
 5 files changed, 42 insertions(+), 50 deletions(-)

diff --git a/src/fPlugin.ml b/src/fPlugin.ml
index 18d3eb9..bcb76ea 100644
--- a/src/fPlugin.ml
+++ b/src/fPlugin.ml
@@ -2,11 +2,10 @@ open CErrors
 open Pp
 open Util
 open Names
+open Decls
 open Term
 open Constr
-open Decl_kinds
 open Libobject
-open Globnames
 open Proofview.Notations
 
 module RelDecl = Context.Rel.Declaration
@@ -76,27 +75,27 @@ let force_solve cat c =
 
 let force_translate_constant cat cst ids =
   let id = match ids with
-  | None -> translate_name (Nametab.basename_of_global (ConstRef cst))
+  | None -> translate_name (Nametab.basename_of_global (GlobRef.ConstRef cst))
   | Some [id] -> id
   | Some _ -> user_err (Pp.str "Not the right number of provided names")
   in
   (* Translate the type *)
   let env = Global.env () in
   let sigma = Evd.from_env env in
-  let typ, _uctx = Typeops.type_of_global_in_context env (ConstRef cst) in
+  let typ, _uctx = Typeops.type_of_global_in_context env (GlobRef.ConstRef cst) in
   let (sigma, typ) = FTranslate.translate_type !translator cat env sigma typ in
   let sigma, _ = Typing.type_of env sigma (EConstr.of_constr typ) in
   (* Define the term by tactic *)
-  let body, _ = Option.get (Global.body_of_constant cst) in
+  let body, _, _ = Option.get (Global.body_of_constant Library.indirect_accessor cst) in
   let (sigma, body) = FTranslate.translate !translator cat env sigma body in
 (*  Pp.pp_with Format.err_formatter (Printer.pr_constr_env env sigma body);*)
   let sigma = Typing.check env sigma (EConstr.of_constr body) (EConstr.of_constr typ) in
   let uctx = Evd.univ_entry ~poly:false sigma in
   let ce = Declare.definition_entry ~types:typ ~univs:uctx body in
-  let cd = Entries.DefinitionEntry ce in
-  let decl = (cd, IsProof Lemma) in
-  let cst_ = Declare.declare_constant id decl in
-  [ConstRef cst, ConstRef cst_]
+  let cd = Declare.DefinitionEntry ce in
+  let kind = IsProof Lemma in
+  let cst_ = Declare.declare_constant ~name:id ~kind cd in
+  [GlobRef.ConstRef cst, GlobRef.ConstRef cst_]
 
 let eta_reduce c =
   let rec aux c =
@@ -120,8 +119,8 @@ let get_mind_globrefs mind =
   let open Declarations in
   let mib = Global.lookup_mind mind in
   let map i body =
-    let ind = IndRef (mind, i) in
-    let map_cons j _ = ConstructRef ((mind, i), j + 1) in
+    let ind = GlobRef.IndRef (mind, i) in
+    let map_cons j _ = GlobRef.ConstructRef ((mind, i), j + 1) in
     ind :: List.mapi map_cons (Array.to_list body.mind_consnames)
   in
   let l = List.mapi map (Array.to_list mib.mind_packets) in
@@ -144,7 +143,7 @@ let force_translate_inductive cat ind ids =
       mib.mind_packets
   in
   let invsubst = List.map NamedDecl.get_id substind in
-  let translator = add_translator !translator (List.map (fun id -> VarRef id, VarRef id) invsubst) in
+  let translator = add_translator !translator (List.map (fun id -> GlobRef.VarRef id, GlobRef.VarRef id) invsubst) in
   (* À chaque inductif I on associe une fonction λp.λparams.λindices.λ(qα), 
      (mkVar I) p params indices *)
   let sigma = Evd.from_env env in
@@ -175,13 +174,11 @@ let force_translate_inductive cat ind ids =
     Array.fold_left fold (sigma, []) mib.mind_packets
   in
   let make_one_entry params body (sigma, bodies_) =
-    let template = match body.mind_arity with
-    | RegularArity _ -> false
-    | TemplateArity _ -> true
-    in
+    (* For template polymorphism, one would need to maintain a substitution of universes *)
+    let template = false in
     (* Heuristic for the return type. Can we do better? *)
     let (sigma, s) =
-      if List.mem Sorts.InType body.mind_kelim then
+      if Sorts.family_leq Sorts.InType body.mind_kelim then
         let sigma, s = Evarutil.new_Type sigma in
         (sigma, EConstr.to_constr sigma s)
       else
@@ -278,11 +275,10 @@ let force_translate_inductive cat ind ids =
     mind_entry_variance = mib.mind_variance;
     mind_entry_private = mib.mind_private;
   } in
-  let (_, kn), _ = Declare.declare_mind mib_ in
-  let mib_ = Global.mind_of_delta_kn kn in
+  let mib_ = DeclareInd.declare_mutual_inductive_with_eliminations mib_ UnivNames.empty_binders [] in
   let map_data gr = match gr with
-  | IndRef (mib, i) -> (gr, IndRef (mib_, i))
-  | ConstructRef ((mib, i), j) -> (gr, ConstructRef ((mib_, i), j))
+  | GlobRef.IndRef (mib, i) -> (gr, GlobRef.IndRef (mib_, i))
+  | GlobRef.ConstructRef ((mib, i), j) -> (gr, GlobRef.ConstructRef ((mib_, i), j))
   | _ -> assert false
   in
   List.map map_data (get_mind_globrefs (fst ind))
@@ -296,8 +292,8 @@ let force_translate (obj, hom) gr ids =
     FTranslate.cat_hom = hom;
   } in
   let ans = match gr with
-  | ConstRef cst -> force_translate_constant cat cst ids
-  | IndRef ind -> force_translate_inductive cat ind ids
+  | GlobRef.ConstRef cst -> force_translate_constant cat cst ids
+  | GlobRef.IndRef ind -> force_translate_inductive cat ind ids
   | _ -> user_err (Pp.str "Translation not handled.")
   in
   let () = Lib.add_anonymous_leaf (in_translator ans) in
@@ -321,25 +317,25 @@ let force_implement (obj, hom) id typ idopt =
   | None -> translate_name id
   | Some id -> id
   in
-  let kind = Global, false, DefinitionBody Definition in
+  let kind = IsDefinition Definition in
+  let scope = DeclareDef.Global Declare.ImportDefaultBehavior in 
   let sigma = Evd.from_env env in
   let (typ, uctx) = Constrintern.interp_type env sigma typ in
   let sigma = Evd.from_ctx uctx in
   let typ = EConstr.to_constr sigma typ in
   let (sigma, typ_) = FTranslate.translate_type !translator cat env sigma typ in
   let (sigma, _) = Typing.type_of env sigma (EConstr.of_constr typ_) in
-  let hook _ _ _ dst =
+  let hook = DeclareDef.Hook.(make (function S.{uctx;dref} ->
     (* Declare the original term as an axiom *)
-    let uctx = Evd.universe_context_set sigma in
-    let param = (None, (typ, Entries.Monomorphic_entry uctx), None) in
-    let cb = Entries.ParameterEntry param in
-    let cst = Declare.declare_constant id (cb, IsDefinition Definition) in
+    let param = (None, (typ, Entries.Monomorphic_entry (UState.context_set uctx)), None) in
+    let cb = Declare.ParameterEntry param in
+    let cst = Declare.declare_constant ~name:id ~kind:(IsDefinition Definition) cb in
     (* Attach the axiom to the forcing implementation *)
-    Lib.add_anonymous_leaf (in_translator [ConstRef cst, dst])
+    Lib.add_anonymous_leaf (in_translator [GlobRef.ConstRef cst, dref])))
   in
-  let hook = Lemmas.mk_hook hook in
   let sigma, _ = Typing.type_of env sigma (EConstr.of_constr typ_) in
-  Lemmas.start_proof ~ontop:None id_ kind sigma (EConstr.of_constr typ_) ~hook
+  let info = Lemmas.Info.make ~hook ~kind ~scope () in
+  Lemmas.start_lemma ~name:id_ ~poly:false ~info sigma (EConstr.of_constr typ_)
 
 (** Error handling *)
 
diff --git a/src/fPlugin.mli b/src/fPlugin.mli
index 2b95ae0..e66f279 100644
--- a/src/fPlugin.mli
+++ b/src/fPlugin.mli
@@ -6,4 +6,4 @@ val force_tac : (EConstr.t * EConstr.t) -> EConstr.t -> unit tactic
 
 val force_translate : (qualid * qualid) -> qualid -> Id.t list option -> unit
 
-val force_implement : (qualid * qualid) -> Id.t -> Constrexpr.constr_expr -> Id.t option -> Proof_global.t
+val force_implement : (qualid * qualid) -> Id.t -> Constrexpr.constr_expr -> Id.t option -> Lemmas.t
diff --git a/src/fTranslate.ml b/src/fTranslate.ml
index ac3ec0a..9e90af4 100644
--- a/src/fTranslate.ml
+++ b/src/fTranslate.ml
@@ -3,7 +3,6 @@ open Term
 open Constr
 open Declarations
 open Environ
-open Globnames
 
 module RelDecl = Context.Rel.Declaration
 
@@ -131,13 +130,13 @@ let translate_var fctx n =
   mkApp (mkRel m, [| p; f |])
 
 let get_inductive fctx ind =
-  let gr = IndRef ind in
+  let gr = GlobRef.IndRef ind in
   let gr_ =
     try GlobRef.Map.find gr fctx.translator
     with Not_found -> raise (MissingGlobal gr)
   in
   match gr_ with
-  | IndRef ind_ -> ind_
+  | GlobRef.IndRef ind_ -> ind_
   | _ -> assert false
 
 let apply_global env sigma gr u fctx =
@@ -150,7 +149,7 @@ let apply_global env sigma gr u fctx =
   let c = EConstr.to_constr sigma c in
   let last = last_condition fctx in
   match gr with
-  | IndRef _ -> assert false
+  | GlobRef.IndRef _ -> assert false
   | _ -> (sigma, mkApp (c, [| mkRel last |]))
 
 (** Forcing translation core *)
@@ -210,13 +209,13 @@ let rec otranslate env fctx sigma c = match kind c with
   let app = mkApp (t_, args_) in
   (sigma, app)
 | Var id ->
-  apply_global env sigma (VarRef id) Univ.Instance.empty fctx
+  apply_global env sigma (GlobRef.VarRef id) Univ.Instance.empty fctx
 | Const (p, u) ->
-  apply_global env sigma (ConstRef p) u fctx
+  apply_global env sigma (GlobRef.ConstRef p) u fctx
 | Ind (ind, u) ->
   otranslate_ind env fctx sigma ind u [||]
 | Construct (c, u) ->
-  apply_global env sigma (ConstructRef c) u fctx
+  apply_global env sigma (GlobRef.ConstructRef c) u fctx
 | Case (ci, r, c, p) ->
    let ind_ = get_inductive fctx ci.ci_ind in
    let ci_ = Inductiveops.make_case_info env ind_ Sorts.Relevant ci.ci_pp_info.style in
@@ -266,6 +265,7 @@ let rec otranslate env fctx sigma c = match kind c with
 | Meta _ -> assert false
 | Evar _ -> assert false
 | Int _ -> assert false
+| Float _ -> assert false
 
 and otranslate_ind env fctx sigma ind u args =
   let ind_ = get_inductive fctx ind in
diff --git a/src/g_forcing.mlg b/src/g_forcing.mlg
index 1e35f35..f26f78b 100644
--- a/src/g_forcing.mlg
+++ b/src/g_forcing.mlg
@@ -22,13 +22,13 @@ END
 
 {
 
-let classify_impl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]), VtLater)
+let classify_impl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]))
 
 }
 
-VERNAC COMMAND EXTEND ForcingImplementation CLASSIFIED BY { classify_impl }
-| ![ proof ] [ "Forcing" "Definition" ident(id) ":" lconstr(typ) "using" global(obj) global(hom) ] ->
-  { fun ~pstate -> Some (FPlugin.force_implement (obj, hom) id typ None) }
-| ![ proof ] [ "Forcing" "Definition" ident(id) ":" lconstr(typ) "as" ident(id') "using" global(obj) global(hom) ] ->
-  { fun ~pstate -> Some (FPlugin.force_implement (obj, hom) id typ (Some id')) }
+VERNAC COMMAND EXTEND ForcingImplementation CLASSIFIED BY { classify_impl } STATE open_proof
+| [ "Forcing" "Definition" ident(id) ":" lconstr(typ) "using" global(obj) global(hom) ] ->
+  { FPlugin.force_implement (obj, hom) id typ None }
+| [ "Forcing" "Definition" ident(id) ":" lconstr(typ) "as" ident(id') "using" global(obj) global(hom) ] ->
+  { FPlugin.force_implement (obj, hom) id typ (Some id') }
 END
diff --git a/theories/Forcing.v b/theories/Forcing.v
index 8ee4584..bddf721 100644
--- a/theories/Forcing.v
+++ b/theories/Forcing.v
@@ -1,6 +1,2 @@
 Declare ML Module "ltac_plugin".
 Declare ML Module "forcing".
-
-(* The plugin is not able to preserve the relation between parameters
-   and conclusions of an inductive type *)
-Global Unset Template Check.

From d0e5197475700437baa0310c5fd0b38ef7fc6080 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Sat, 5 Jun 2021 15:56:19 +0200
Subject: [PATCH 6/8] Updating to Coq 8.12

---
 src/fPlugin.ml | 22 ++++++++++------------
 1 file changed, 10 insertions(+), 12 deletions(-)

diff --git a/src/fPlugin.ml b/src/fPlugin.ml
index bcb76ea..a6de2a3 100644
--- a/src/fPlugin.ml
+++ b/src/fPlugin.ml
@@ -31,7 +31,7 @@ let cache_translator (_, l) =
   translator := add_translator !translator l
 
 let load_translator _ l = cache_translator l
-let open_translator _ l = cache_translator l
+let open_translator _ _ l = cache_translator l
 
 let in_translator : translator_obj -> obj =
   declare_object { (default_object "FORCING TRANSLATOR") with
@@ -139,7 +139,7 @@ let force_translate_inductive cat ind ids =
   let substind =
     Array.map_to_list (fun oib ->
         NamedDecl.LocalAssum (Context.annotR oib.mind_typename,
-			      Inductive.type_of_inductive env ((mib, oib), Univ.Instance.empty)))
+			      Inductive.type_of_inductive ((mib, oib), Univ.Instance.empty)))
       mib.mind_packets
   in
   let invsubst = List.map NamedDecl.get_id substind in
@@ -174,8 +174,6 @@ let force_translate_inductive cat ind ids =
     Array.fold_left fold (sigma, []) mib.mind_packets
   in
   let make_one_entry params body (sigma, bodies_) =
-    (* For template polymorphism, one would need to maintain a substitution of universes *)
-    let template = false in
     (* Heuristic for the return type. Can we do better? *)
     let (sigma, s) =
       if Sorts.family_leq Sorts.InType body.mind_kelim then
@@ -236,14 +234,13 @@ let force_translate_inductive cat ind ids =
     let body_ = {
       mind_entry_typename = typename;
       mind_entry_arity = arity;
-      mind_entry_template = template;
       mind_entry_consnames = consnames;
       mind_entry_lc = List.rev lc_;
     } in
-
-
     (sigma, body_ :: bodies_)
   in
+  (* For template polymorphism, one would need to maintain a substitution of universes *)
+  let template = false in
   (* We proceed to the whole mutual block *)
   let record = match mib.mind_record with
   | NotRecord -> None
@@ -272,7 +269,8 @@ let force_translate_inductive cat ind ids =
     mind_entry_params = params_;
     mind_entry_inds = bodies_;
     mind_entry_universes = uctx;
-    mind_entry_variance = mib.mind_variance;
+    mind_entry_template = template;
+    mind_entry_cumulative = Option.has_some mib.mind_variance;
     mind_entry_private = mib.mind_private;
   } in
   let mib_ = DeclareInd.declare_mutual_inductive_with_eliminations mib_ UnivNames.empty_binders [] in
@@ -318,14 +316,14 @@ let force_implement (obj, hom) id typ idopt =
   | Some id -> id
   in
   let kind = IsDefinition Definition in
-  let scope = DeclareDef.Global Declare.ImportDefaultBehavior in 
+  let scope = Declare.Global Declare.ImportDefaultBehavior in 
   let sigma = Evd.from_env env in
   let (typ, uctx) = Constrintern.interp_type env sigma typ in
   let sigma = Evd.from_ctx uctx in
   let typ = EConstr.to_constr sigma typ in
   let (sigma, typ_) = FTranslate.translate_type !translator cat env sigma typ in
   let (sigma, _) = Typing.type_of env sigma (EConstr.of_constr typ_) in
-  let hook = DeclareDef.Hook.(make (function S.{uctx;dref} ->
+  let hook = Declare.Hook.(make (function S.{uctx;dref} ->
     (* Declare the original term as an axiom *)
     let param = (None, (typ, Entries.Monomorphic_entry (UState.context_set uctx)), None) in
     let cb = Declare.ParameterEntry param in
@@ -342,6 +340,6 @@ let force_implement (obj, hom) id typ idopt =
 let _ = register_handler begin function
 | FTranslate.MissingGlobal gr ->
   let ref = Nametab.shortest_qualid_of_global Id.Set.empty gr in
-  str "No forcing translation for global " ++ Libnames.pr_qualid ref ++ str "."
-| _ -> raise Unhandled
+  Some (str "No forcing translation for global " ++ Libnames.pr_qualid ref ++ str ".")
+| _ -> None
 end

From 8fb4688c87eb6991cde08689c51b4c1337fbb491 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Sat, 5 Jun 2021 16:07:34 +0200
Subject: [PATCH 7/8] Updating to Coq 8.13

---
 src/fPlugin.ml    | 7 ++++---
 src/fPlugin.mli   | 2 +-
 src/fTranslate.ml | 7 +++++--
 3 files changed, 10 insertions(+), 6 deletions(-)

diff --git a/src/fPlugin.ml b/src/fPlugin.ml
index a6de2a3..f4f3d4e 100644
--- a/src/fPlugin.ml
+++ b/src/fPlugin.ml
@@ -316,7 +316,7 @@ let force_implement (obj, hom) id typ idopt =
   | Some id -> id
   in
   let kind = IsDefinition Definition in
-  let scope = Declare.Global Declare.ImportDefaultBehavior in 
+  let scope = Locality.(Global ImportDefaultBehavior) in 
   let sigma = Evd.from_env env in
   let (typ, uctx) = Constrintern.interp_type env sigma typ in
   let sigma = Evd.from_ctx uctx in
@@ -332,8 +332,9 @@ let force_implement (obj, hom) id typ idopt =
     Lib.add_anonymous_leaf (in_translator [GlobRef.ConstRef cst, dref])))
   in
   let sigma, _ = Typing.type_of env sigma (EConstr.of_constr typ_) in
-  let info = Lemmas.Info.make ~hook ~kind ~scope () in
-  Lemmas.start_lemma ~name:id_ ~poly:false ~info sigma (EConstr.of_constr typ_)
+  let info = Declare.Info.make ~hook ~kind ~scope ~poly:false () in
+  let cinfo = Declare.CInfo.make ~name:id_ ~typ:(EConstr.of_constr typ_) () in
+  Declare.Proof.start ~cinfo ~info sigma 
 
 (** Error handling *)
 
diff --git a/src/fPlugin.mli b/src/fPlugin.mli
index e66f279..0597f3b 100644
--- a/src/fPlugin.mli
+++ b/src/fPlugin.mli
@@ -6,4 +6,4 @@ val force_tac : (EConstr.t * EConstr.t) -> EConstr.t -> unit tactic
 
 val force_translate : (qualid * qualid) -> qualid -> Id.t list option -> unit
 
-val force_implement : (qualid * qualid) -> Id.t -> Constrexpr.constr_expr -> Id.t option -> Lemmas.t
+val force_implement : (qualid * qualid) -> Id.t -> Constrexpr.constr_expr -> Id.t option -> Declare.Proof.t
diff --git a/src/fTranslate.ml b/src/fTranslate.ml
index 9e90af4..53fc0c4 100644
--- a/src/fTranslate.ml
+++ b/src/fTranslate.ml
@@ -216,7 +216,7 @@ let rec otranslate env fctx sigma c = match kind c with
   otranslate_ind env fctx sigma ind u [||]
 | Construct (c, u) ->
   apply_global env sigma (GlobRef.ConstructRef c) u fctx
-| Case (ci, r, c, p) ->
+| Case (ci, r, iv, c, p) ->
    let ind_ = get_inductive fctx ci.ci_ind in
    let ci_ = Inductiveops.make_case_info env ind_ Sorts.Relevant ci.ci_pp_info.style in
    let (sigma, c_) = otranslate env fctx sigma c in
@@ -258,7 +258,9 @@ let rec otranslate env fctx sigma c = match kind c with
    let (sigma, r_) = fix_return_clause env fctx sigma r in
    let fold sigma u = otranslate env fctx sigma u in
    let (sigma, p_) = CArray.fold_left_map fold sigma p in
-   (sigma, mkCase (ci_, r_, c_, p_))
+   (* Do not support "UIP" *)
+   let iv_ = NoInvert in
+   (sigma, mkCase (ci_, r_, iv_, c_, p_))
 | Fix f -> assert false
 | CoFix f -> assert false
 | Proj (p, c) -> assert false
@@ -266,6 +268,7 @@ let rec otranslate env fctx sigma c = match kind c with
 | Evar _ -> assert false
 | Int _ -> assert false
 | Float _ -> assert false
+| Array _ -> assert false
 
 and otranslate_ind env fctx sigma ind u args =
   let ind_ = get_inductive fctx ind in

From 609d11e2569724b5c5fe8fec52eb793f3cc29c4c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Sat, 5 Jun 2021 17:30:00 +0200
Subject: [PATCH 8/8] Fixing issue #6: forcing of singleton Prop.

---
 src/fPlugin.ml | 13 +++++++------
 test/Test.v    |  5 ++++-
 2 files changed, 11 insertions(+), 7 deletions(-)

diff --git a/src/fPlugin.ml b/src/fPlugin.ml
index f4f3d4e..59b5277 100644
--- a/src/fPlugin.ml
+++ b/src/fPlugin.ml
@@ -174,13 +174,14 @@ let force_translate_inductive cat ind ids =
     Array.fold_left fold (sigma, []) mib.mind_packets
   in
   let make_one_entry params body (sigma, bodies_) =
-    (* Heuristic for the return type. Can we do better? *)
     let (sigma, s) =
-      if Sorts.family_leq Sorts.InType body.mind_kelim then
-        let sigma, s = Evarutil.new_Type sigma in
-        (sigma, EConstr.to_constr sigma s)
-      else
-        (sigma, mkProp)
+      match body.mind_arity with
+      | RegularArity {mind_sort=s} when Sorts.(is_prop s || is_sprop s) ->
+         (* Impredicative sorts are stable by quantification over forcing conditions *)
+         (sigma, mkSort s)
+      | _ ->
+         let sigma, s = Evarutil.new_Type sigma in
+         (sigma, EConstr.to_constr sigma s)
     in
     let (sigma, arity) =
       (* On obtient l'arité de l'inductif en traduisant le type de chaque indice
diff --git a/test/Test.v b/test/Test.v
index da072e7..5ff8377 100644
--- a/test/Test.v
+++ b/test/Test.v
@@ -27,4 +27,7 @@ _force (fun A n (v : vect A n) =>
             |consv _ _ x r => 1 
           end).
 exact I.
-Qed.
\ No newline at end of file
+Qed.
+
+Forcing Translate and using Obj Hom.
+Forcing Translate iff using Obj Hom.