Backport 8.19 to 8.18 branch, some ML-side incompatibilities

benchmarks/lib/Makefile

@@ -7,7 +7,7 @@
 ##         #     GNU Lesser General Public License Version 2.1          ##
 ##         #     (see LICENSE file for the text of the license)         ##
 ##########################################################################
-## GNUMakefile for Coq 8.19.1
+## GNUMakefile for Coq 8.18.0
 
 # For debugging purposes (must stay here, don't move below)
 INITIAL_VARS := $(.VARIABLES)
@@ -278,7 +278,7 @@ COQDOCLIBS?=$(COQLIBS_NOML)
 # The version of Coq being run and the version of coq_makefile that
 # generated this makefile
 COQ_VERSION:=$(shell $(COQC) --print-version | cut -d " " -f 1)
-COQMAKEFILE_VERSION:=8.19.1
+COQMAKEFILE_VERSION:=8.18.0
 
 # COQ_SRC_SUBDIRS is for user-overriding, usually to add
 # `user-contrib/Foo` to the includes, we keep COQCORE_SRC_SUBDIRS for
@@ -307,14 +307,6 @@ else
   TIMING_ARG=
 endif
 
-ifneq (,$(PROFILING))
-  PROFILE_ARG=-profile $<.prof.json
-  PROFILE_ZIP=gzip $<.prof.json
-else
-  PROFILE_ARG=
-  PROFILE_ZIP=true
-endif
-
 # Files #######################################################################
 #
 # We here define a bunch of variables about the files being part of the
@@ -816,22 +808,20 @@ ifneq (,$(filter grouped-target,$(.FEATURES)))
 define globvorule=
 
 # take care to $$ variables using $< etc
-  $(1).vo $(1).glob &: $(1).v | $$(VDFILE)
-	$$(SHOW)COQC $(1).v
-	$$(HIDE)$$(TIMER) $$(COQC) $$(COQDEBUG) $$(TIMING_ARG) $$(PROFILE_ARG) $$(COQFLAGS) $$(COQLIBS) $(1).v
-	$$(HIDE)$$(PROFILE_ZIP)
+  $(1).vo $(1).glob &: $(1).v | $(VDFILE)
+	$(SHOW)COQC $(1).v
+	$(HIDE)$$(TIMER) $(COQC) $(COQDEBUG) $$(TIMING_ARG) $(COQFLAGS) $(COQLIBS) $(1).v
 ifeq ($(COQDONATIVE), "yes")
-	$$(SHOW)COQNATIVE $(1).vo
-	$$(HIDE)$$(call TIMER,$(1).vo.native) $$(COQNATIVE) $$(COQLIBS) $(1).vo
+	$(SHOW)COQNATIVE $(1).vo
+	$(HIDE)$(call TIMER,$(1).vo.native) $(COQNATIVE) $(COQLIBS) $(1).vo
 endif
 
 endef
 else
 
 $(VOFILES): %.vo: %.v | $(VDFILE)
 	$(SHOW)COQC $<
-	$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(PROFILE_ARG) $(COQFLAGS) $(COQLIBS) $<
-	$(HIDE)$(PROFILE_ZIP)
+	$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $(COQLIBS) $<
 ifeq ($(COQDONATIVE), "yes")
 	$(SHOW)COQNATIVE $@
 	$(HIDE)$(call TIMER,[email protected]) $(COQNATIVE) $(COQLIBS) $@

cplugin/certicoq.ml

@@ -674,8 +674,8 @@ module CompileFunctor (CI : CompilerInterface) = struct
     | Unix.WSIGNALED n | Unix.WSTOPPED n -> CErrors.user_err Pp.(str"Compiler was signaled with code " ++ int n  ++ str" while running " ++ str cmd)
 
   type reifyable_type =
-  | IsInductive of Names.inductive * UVars.Instance.t * Constr.t list
-  | IsPrimitive of Names.Constant.t * UVars.Instance.t * Constr.t list
+  | IsInductive of Names.inductive * Univ.Instance.t * Constr.t list
+  | IsPrimitive of Names.Constant.t * Univ.Instance.t * Constr.t list
 
   let type_of_reifyable_type = function
     | IsInductive (hd, u, args) -> Term.applistc (Constr.mkIndU ((hd, u))) args

cplugin/tm_util.ml

@@ -134,7 +134,7 @@ module CaseCompat =
       let realdecls, _ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in
       let self =
         let args = Context.Rel.instance mkRel 0 mip.mind_arity_ctxt in
-        let inst = UVars.Instance.abstract_instance (UVars.Instance.length u) in
+        let inst = Instance.of_array (Array.init (Instance.length u) Level.var) in
         mkApp (mkIndU (ci.ci_ind, inst), args)
       in
       let realdecls = LocalAssum (Context.anonR, self) :: realdecls in

plugin/certicoq.ml

@@ -587,8 +587,8 @@ module CompileFunctor (CI : CompilerInterface) = struct
     | Unix.WSIGNALED n | Unix.WSTOPPED n -> CErrors.user_err Pp.(str"Compiler was signaled with code " ++ int n  ++ str" while running " ++ str cmd)
 
   type reifyable_type =
-  | IsInductive of Names.inductive * UVars.Instance.t * Constr.t list
-  | IsPrimitive of Names.Constant.t * UVars.Instance.t * Constr.t list
+  | IsInductive of Names.inductive * Univ.Instance.t * Constr.t list
+  | IsPrimitive of Names.Constant.t * Univ.Instance.t * Constr.t list
 
   let type_of_reifyable_type = function
     | IsInductive (hd, u, args) -> Term.applistc (Constr.mkIndU ((hd, u))) args

plugin/tm_util.ml

@@ -132,7 +132,7 @@ module CaseCompat =
       let realdecls, _ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in
       let self =
         let args = Context.Rel.instance mkRel 0 mip.mind_arity_ctxt in
-        let inst = UVars.Instance.abstract_instance (UVars.Instance.length u) in
+        let inst = Instance.of_array (Array.init (Instance.length u) Level.var) in
         mkApp (mkIndU (ci.ci_ind, inst), args)
       in
       let realdecls = LocalAssum (Context.anonR, self) :: realdecls in

theories/LambdaANF/closure_conversion_correct.v

@@ -565,7 +565,7 @@ Section Closure_conversion_correct.
     n <= n * m.
   Proof.
     rewrite Nat.mul_comm.
-    edestruct Arith_base.mult_O_le_stt; eauto. lia.
+    edestruct Arith_prebase.mult_O_le_stt; eauto. lia.
   Qed.
 
   Lemma plus_le_mult  (a1 a2 b1 b2 b3 : nat) :

theories/LambdaBoxLocal/LambdaBoxMut_to_LambdaBoxLocal_correct.v

@@ -1284,7 +1284,7 @@ Lemma LambdaBoxMutsbst_fix_preserves_lam dts nm bod :
 Proof.
   revert nm bod; induction (list_to_zero (dlength dts)); simpl; intros.
   reflexivity.
- (* simpl. rewrite LambdaBoxMut.term.instantiate_TLambda. *)
+  simpl. rewrite LambdaBoxMut.term.instantiate_TLambda.
   simpl. rewrite IHl. reflexivity.
 Qed.
 

theories/LambdaBoxLocal/expression.v

@@ -649,7 +649,7 @@ Qed.
 Declare Scope name.
 Bind Scope name with name.
 Delimit Scope name with name.
-Arguments nNamed i%_bs.
+Arguments nNamed i%bs.
 Definition nNameds (s : string) : name := nNamed s.
 
 Notation " [: x ] " := (cons (nNameds x) nil) : name.
@@ -658,8 +658,8 @@ Notation " '[:' x , y , .. , z ] " :=
 Local Open Scope name.
 
 Coercion nNameds : string >-> name.
-Arguments Lam_e n%_bs _.
-Arguments eflcons n%_bs _ _.
+Arguments Lam_e n%bs _.
+Arguments eflcons n%bs _ _.
 
 Example x1: exp := Lam_e "x" (Var_e 0).  (* identity *)
 Lemma Lx1: forall (e d:exp), eval e d -> eval (App_e x1 e) d.

theories/LambdaBoxMut/stripEvalCommute.v

@@ -788,15 +788,15 @@ Proof.
     move/andP: H0 => [] /andP[] wfi wft wfl.
     set (brs' := map _ l). cbn in brs'.
     set (brs'0 := map _ l). simpl.
-(*    rewrite instantiate_TCase. *) rtoProp; intuition auto. f_equal; eauto.
+   rewrite instantiate_TCase. rtoProp; intuition auto. f_equal; eauto.
     clear -X wfl.
     { subst brs' brs'0. repeat toAll. induction wfl.
     - constructor.
     - cbn -[instantiateBrs]. rewrite instantiateBrs_equation.
       f_equal; eauto. destruct p. rewrite List.rev_length. repeat eapply (e n).
       eapply wellformed_up; tea. lia. }
   - rewrite map_map_compose. set (mfix' := map _ m).
-    simpl. (*rewrite instantiate_TFix. *) f_equal.
+    simpl. rewrite instantiate_TFix. f_equal.
     clear -X H.
     move/andP: H => [] _ /andP[] _ H1. repeat toAll.
     rewrite -dlength_hom. 

theories/common/AstCommon.v

@@ -18,7 +18,7 @@ Set Implicit Arguments.
 Ltac inv H := inversion H; subst; clear H.
 
 (** Fix arguments scope for [mkInd]. *)
-Arguments mkInd _%_bs _%_nat.
+Arguments mkInd _%bs _%nat.
 
 (** Use with caution, valid kernames from Coq cannot have an empty MPFile component. *)
 Definition kername_of_string (s : string) := (MPfile nil, s).

theories/common/exceptionMonad.v

@@ -5,11 +5,11 @@ Import MonadNotation.
 
 Inductive exception (A:Type) := Exc (_:string) | Ret (_:A).
 Arguments Ret [A].
-Arguments Exc [A] _%_bs.
+Arguments Exc [A] _%bs.
 
 Definition ret {A: Type} (x: A) := Ret x.
 Definition raise {A: Type} (str:string) := @Exc A str.
-Arguments raise {A} _%_bs.
+Arguments raise {A} _%bs.
 
 Definition bind
     {A B: Type} (a: exception A) (f: A -> exception B): exception B :=