porting to 8.8

Makefile.local

@@ -2,6 +2,7 @@
 #RED='\033[0;31m'
 #NC='\033[0m' # No Color
 #COQC=coqc
+COQ_SRC_SUBDIRS+=user-contrib/Unicoq
 
 TESTS=$(wildcard tests/*.v)
 TESTRESULTS=$(TESTS:.v=.vo)

_CoqProject

@@ -1,6 +1,5 @@
 CAMLC = "ocamlc -c -rectypes -thread -warn-error +a"
 CAMLDEBUG = "-g"
--I $(COQMF_COQLIB)/user-contrib/Unicoq
 -I src
 -R theories Mtac2
 -Q tests Mtac2Tests
@@ -12,8 +11,6 @@ src/mtacNames.ml
 src/mtacNames.mli
 src/mConstr.ml
 src/mConstr.mli
-src/machine.ml
-src/machine.mli
 src/run.ml
 src/run.mli
 src/metaCoqInterp.ml

src/MetaCoqPlugin.mlpack

@@ -3,7 +3,6 @@ MetaCoqInstr
 Constrs
 MtacNames
 MConstr
-Machine
 Run
 MetaCoqInterp
 MetaCoqInit

src/constrs.ml

@@ -9,7 +9,7 @@ let decompose_appvect sigma c =
   | App (f,cl) -> (f, cl)
   | _ -> (c,[||])
 
-module Constr = struct
+module Constrs = struct
   exception Constr_not_found of string
   exception Constr_poly of string
 
@@ -34,30 +34,34 @@ module Constr = struct
 end
 
 module ConstrBuilder = struct
+  open Constrs
+
   type t = string
 
   let from_string (s:string) : t = s
 
-  let build s = Lazy.force (Constr.mkConstr s)
-  let build_app s args = mkApp (Lazy.force (Constr.mkConstr s), args)
+  let build s = Lazy.force (mkConstr s)
+  let build_app s args = mkApp (Lazy.force (mkConstr s), args)
 
-  let equal sigma s = Constr.isConstr sigma (Constr.mkConstr s)
+  let equal sigma s = isConstr sigma (mkConstr s)
 
   let from_coq s (_, sigma) cterm =
     let (head, args) = decompose_appvect sigma cterm in
     if equal sigma s head then Some args else None
 end
 
 module UConstrBuilder = struct
+  open Constrs
+
   type t = string
 
   let from_string (s:string) : t = s
 
   let build_app s sigma env args =
-    let (sigma, c) = Constr.mkUConstr s sigma env in
+    let (sigma, c) = mkUConstr s sigma env in
     (sigma, mkApp (c, args))
 
-  let equal = Constr.isUConstr
+  let equal = isUConstr
 
   let from_coq s (env, sigma) cterm =
     let (head, args) = decompose_appvect sigma cterm in
@@ -190,13 +194,15 @@ module CoqSig = struct
 end
 
 module CoqPositive = struct
-  let xI = Constr.mkConstr "Coq.Numbers.BinNums.xI"
-  let xO = Constr.mkConstr "Coq.Numbers.BinNums.xO"
-  let xH = Constr.mkConstr "Coq.Numbers.BinNums.xH"
+  open Constrs
 
-  let isH sigma = Constr.isConstr sigma xH
-  let isI sigma = Constr.isConstr sigma xI
-  let isO sigma = Constr.isConstr sigma xO
+  let xI = mkConstr "Coq.Numbers.BinNums.xI"
+  let xO = mkConstr "Coq.Numbers.BinNums.xO"
+  let xH = mkConstr "Coq.Numbers.BinNums.xH"
+
+  let isH sigma = isConstr sigma xH
+  let isI sigma = isConstr sigma xI
+  let isO sigma = isConstr sigma xO
 
   let from_coq (env, evd) c =
     let rec fc i c =
@@ -226,12 +232,13 @@ module CoqPositive = struct
 end
 
 module CoqN = struct
+  open Constrs
   (* let tN = Constr.mkConstr "Coq.Numbers.BinNums.N" *)
-  let h0 = Constr.mkConstr "Coq.Numbers.BinNums.N0"
-  let hP = Constr.mkConstr "Coq.Numbers.BinNums.Npos"
+  let h0 = mkConstr "Coq.Numbers.BinNums.N0"
+  let hP = mkConstr "Coq.Numbers.BinNums.Npos"
 
-  let is0 sigma = Constr.isConstr sigma h0
-  let isP sigma = Constr.isConstr sigma hP
+  let is0 sigma = isConstr sigma h0
+  let isP sigma = isConstr sigma hP
 
   exception NotAnN
 
@@ -259,9 +266,11 @@ module CoqN = struct
 end
 
 module CoqZ = struct
-  let z0 = Constr.mkConstr "Coq.Numbers.BinNums.Z0"
-  let zpos = Constr.mkConstr "Coq.Numbers.BinNums.Zpos"
-  let zneg = Constr.mkConstr "Coq.Numbers.BinNums.Zneg"
+  open Constrs
+
+  let z0 = mkConstr "Coq.Numbers.BinNums.Z0"
+  let zpos = mkConstr "Coq.Numbers.BinNums.Zpos"
+  let zneg = mkConstr "Coq.Numbers.BinNums.Zneg"
 
   let to_coq n =
     if n = 0 then
@@ -362,7 +371,7 @@ module MCTactics = struct
   let mkUConstr s env sigma =
     let open Nametab in let open Libnames in
     try Evd.fresh_global env sigma (locate (qualid_of_string s))
-    with _ -> raise (Constr.Constr_not_found s)
+    with _ -> raise (Constrs.Constr_not_found s)
 
   let mkGTactic = mkUConstr gTactic
 end

src/constrs.mli

@@ -3,7 +3,7 @@ open EConstr
 
 val decompose_appvect : evar_map -> constr -> constr * constr array
 
-module Constr : sig
+module Constrs : sig
   exception Constr_not_found of string
   exception Constr_poly of string
 
@@ -121,6 +121,7 @@ module CoqSig : sig
 end
 
 module MCTactics : sig
+  [@@@warning "-3"] (* Term.constr is deprecated in favor of Constr.t, but Constr.t is not accessible to the compiler for some reason :-/ *)
   val mkGTactic : Environ.env -> Evd.evar_map -> Evd.evar_map * Term.constr
 end
 

src/machine.ml

@@ -8,7 +8,7 @@
 
 open Util
 open Names
-open Term
+open Constr
 open Termops
 open Univ
 open Evd
@@ -111,16 +111,16 @@ module Stack :
 sig
   open EConstr
   type 'a app_node
-  val pr_app_node : ('a -> Pp.std_ppcmds) -> 'a app_node -> Pp.std_ppcmds
+  val pr_app_node : ('a -> Pp.t) -> 'a app_node -> Pp.t
 
   type cst_member =
     | Cst_const of pconstant
-    | Cst_proj of projection
+    | Cst_proj of Projection.t
 
   type 'a member =
     | App of 'a app_node
     | Case of case_info * 'a * 'a array * Cst_stack.t
-    | Proj of int * int * projection * Cst_stack.t
+    | Proj of int * int * Projection.t * Cst_stack.t
     | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t
     | Cst of cst_member * int * int list * 'a t * Cst_stack.t
     | Shift of int
@@ -129,7 +129,7 @@ sig
 
   exception IncompatibleFold2
 
-  val pr : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds
+  val pr : ('a -> Pp.t) -> 'a t -> Pp.t
   val empty : 'a t
   val is_empty : 'a t -> bool
   val append_app : 'a array -> 'a t -> 'a t
@@ -168,12 +168,12 @@ struct
 
   type cst_member =
     | Cst_const of pconstant
-    | Cst_proj of projection
+    | Cst_proj of Projection.t
 
   type 'a member =
     | App of 'a app_node
-    | Case of Term.case_info * 'a * 'a array * Cst_stack.t
-    | Proj of int * int * projection * Cst_stack.t
+    | Case of case_info * 'a * 'a array * Cst_stack.t
+    | Proj of int * int * Projection.t * Cst_stack.t
     | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t
     | Cst of cst_member * int * int list * 'a t * Cst_stack.t
     | Shift of int
@@ -191,7 +191,7 @@ struct
         ++ str ")"
     | Proj (n,m,p,cst) ->
         str "ZProj(" ++ int n ++ pr_comma () ++ int m ++
-        pr_comma () ++ pr_con (Projection.constant p) ++ str ")"
+        pr_comma () ++ Constant.print (Projection.constant p) ++ str ")"
     | Fix (f,args,cst) ->
         str "ZFix(" ++ Termops.pr_fix pr_c f
         ++ pr_comma () ++ pr pr_c args ++ str ")"
@@ -468,7 +468,7 @@ let magicaly_constant_of_fixbody env sigma reference bd = function
         match constant_opt_value_in env (cst,u) with
         | None -> bd
         | Some t ->
-            let csts = EConstr.eq_constr_universes sigma (EConstr.of_constr t) bd in
+            let csts = EConstr.eq_constr_universes env sigma (EConstr.of_constr t) bd in
             begin match csts with
             | Some csts ->
                 let subst = Universes.Constraints.fold (fun (l,d,r) acc ->

src/machine.mli

@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Names
-open Term
+open Constr
 open EConstr
 open Evd
 (* open Environ *)
@@ -62,30 +62,30 @@ module Cst_stack : sig
   val best_cst : t -> (constr * constr list) option
   val best_replace : Evd.evar_map -> constr -> t -> constr -> constr
   val reference : Evd.evar_map -> t -> Constant.t option
-  val pr : t -> Pp.std_ppcmds
+  val pr : t -> Pp.t
 end
 
 module Stack : sig
   type 'a app_node
 
-  val pr_app_node : ('a -> Pp.std_ppcmds) -> 'a app_node -> Pp.std_ppcmds
+  val pr_app_node : ('a -> Pp.t) -> 'a app_node -> Pp.t
 
   type cst_member =
     | Cst_const of pconstant
-    | Cst_proj of projection
+    | Cst_proj of Projection.t
 
   type 'a member =
     | App of 'a app_node
     | Case of case_info * 'a * 'a array * Cst_stack.t
-    | Proj of int * int * projection * Cst_stack.t
+    | Proj of int * int * Projection.t * Cst_stack.t
     | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t
     | Cst of cst_member * int (** current foccussed arg *) * int list (** remaining args *)
              * 'a t * Cst_stack.t
     | Shift of int
     | Update of 'a
   and 'a t = 'a member list
 
-  val pr : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds
+  val pr : ('a -> Pp.t) -> 'a t -> Pp.t
 
   val empty : 'a t
   val is_empty : 'a t -> bool

src/metaCoqInterp.ml

@@ -1,5 +1,6 @@
 open Constrs
 open Pp
+open Ltac_pretype
 
 module MetaCoqRun = struct
   (** This module run the interpretation of a constr
@@ -18,7 +19,7 @@ module MetaCoqRun = struct
 
   let ifTactic env sigma ty c =
     let (sigma, gtactic) = MCTactics.mkGTactic env sigma in
-    let unitType = Constrs.CoqUnit.mkType in
+    let unitType = CoqUnit.mkType in
     let gtactic = EConstr.mkApp(EConstr.of_constr gtactic, [|unitType|]) in
     let open Evarsolve in
     let res = Munify.unify_evar_conv Names.full_transparent_state env sigma Reduction.CONV gtactic ty in
@@ -51,20 +52,20 @@ module MetaCoqRun = struct
         if not istactic then
           Refine.refine ~typecheck:false begin fun evd -> evd, v end
         else
-          let goals = Constrs.CoqList.from_coq sigma env v in
-          let goals = List.map (fun x -> snd (Constrs.CoqPair.from_coq (env, sigma) x)) goals in
+          let goals = CoqList.from_coq sigma env v in
+          let goals = List.map (fun x -> snd (CoqPair.from_coq (env, sigma) x)) goals in
           let goals = List.map (Run.Goal.evar_of_goal sigma env) goals in
           let goals = List.filter Option.has_some goals in
-          let goals = List.map Option.get goals in
+          let goals = List.map (fun e->Proofview_monad.with_empty_state (Option.get e)) goals in
           Unsafe.tclSETGOALS goals
 
     | Run.Err (_, e) ->
         CErrors.user_err (str "Uncaught exception: " ++ (Termops.print_constr e))
 
   let evar_of_goal gl =
     let open Proofview.Goal in
-    let ids = List.map (fun d->Term.mkVar (Context.Named.Declaration.get_id d)) (Environ.named_context (env gl)) in
-    Term.mkEvar (goal gl, Array.of_list ids)
+    let ids = List.map (fun d->Constr.mkVar (Context.Named.Declaration.get_id d)) (Environ.named_context (env gl)) in
+    Constr.mkEvar (goal gl, Array.of_list ids)
 
   (** Get back the context given a goal, interp the constr_expr to obtain a constr
       Then run the interpretation fo the constr, and returns the tactic value,
@@ -82,9 +83,8 @@ module MetaCoqRun = struct
     end
 
 
-  let understand env sigma {Glob_term.closure=closure;term=term} =
+  let understand env sigma {closure=closure;term=term} =
     let open Glob_ops in
-    let open Glob_term in
     let open Pretyping in
     let flags = all_no_fail_flags in
     let lvar = { empty_lvar with
@@ -126,13 +126,13 @@ end
     - Print subgoals *)
 [@@@ocaml.warning "-3"] (* deprecated use of set_proof_mode *)
 let interp_mproof_command () =
-  let pf = Proof_global.give_me_the_proof () in
-  if Proof.is_done pf then
+  let proof = Proof_global.give_me_the_proof () in
+  if Proof.is_done proof then
     CErrors.user_err (str "Nothing left to prove here.")
   else
     begin
       Proof_global.set_proof_mode "MProof";
-      Feedback.msg_info @@ Printer.pr_open_subgoals ();
+      Feedback.msg_info @@ Printer.pr_open_subgoals ~proof;
     end
 
 (** Interpreter of a mtactic *)
@@ -182,4 +182,4 @@ let end_proof () =
     remove_dangling_evars ();
   (* The following invokes the usual Qed. *)
   let open Vernacexpr in
-  Lemmas.save_proof (Proved (Opaque None,None))
+  Lemmas.save_proof (Proved (Opaque,None))

src/metaCoqInterp.mli

@@ -1,5 +1,7 @@
+open Ltac_pretype
+
 module MetaCoqRun : sig
-  val run_tac_constr : Glob_term.closed_glob_constr -> unit Proofview.tactic
+  val run_tac_constr : closed_glob_constr -> unit Proofview.tactic
 
   val run_cmd : Constrexpr.constr_expr -> unit
 end

src/mtacNames.ml

@@ -4,12 +4,12 @@ open Termops
 open Constrs
 
 let metaCoq_module_name = "Mtac2.intf"
-let mkConstr e = Constr.mkConstr (metaCoq_module_name ^ "." ^ e)
-let mkUConstr e = Constr.mkUConstr (metaCoq_module_name ^ "." ^ e)
+let mkConstr e = Constrs.mkConstr (metaCoq_module_name ^ "." ^ e)
+let mkUConstr e = Constrs.mkUConstr (metaCoq_module_name ^ "." ^ e)
 let mkBuilder e = ConstrBuilder.from_string (metaCoq_module_name ^ "." ^ e)
 let mkUBuilder e = UConstrBuilder.from_string (metaCoq_module_name ^ "." ^ e)
 let mkT_lazy = mkUConstr "M.M.t"
-let mkUConstr e = Constr.mkUConstr (metaCoq_module_name ^ "." ^ e)
+let mkUConstr e = Constrs.mkUConstr (metaCoq_module_name ^ "." ^ e)
 
 let isConstr sigma e =
   let c = Lazy.force (mkConstr e) in