diff --git a/.github/workflows/latest.yml b/.github/workflows/latest.yml
index 30bc5badf..94c6ba7a1 100644
--- a/.github/workflows/latest.yml
+++ b/.github/workflows/latest.yml
@@ -19,7 +19,7 @@ jobs:
       opamroot: /home/rocq/.opam
       configopts: -ignore-coq-version
     container:
-      image: rocq/rocq-prover:9.1.1
+      image: rocq/rocq-prover:9.2.0
       options: --user root
     steps:
       - name: Checkout
@@ -27,7 +27,7 @@ jobs:
         with:
           submodules: true
       - name: OPAM dependencies
-        run: tools/runner.sh opam_install coq menhir
+        run: tools/runner.sh opam_install rocq-prover menhir
       - name: Configure
         run: tools/runner.sh configure
       - name: Build
diff --git a/Makefile b/Makefile
index 82af3678a..a5b1cbd1f 100644
--- a/Makefile
+++ b/Makefile
@@ -51,33 +51,53 @@ endif
 # unused-pattern-matching-variable:
 #    warning introduced in 8.13
 #    the code rewrite that avoids the warning is not desirable
-# undeclared-scope:
-#    warning introduced in 8.12, addressed in the main CompCert files
-#    triggered by MenhirLib, to be solved upstream
-# deprecated-instance-without-locality:
-#    warning introduced in 8.14
-#    triggered by Menhir-generated files, to be solved upstream in Menhir
 # deprecated-since-8.19
 # deprecated-since-8.20
+# deprecated-reference-since-9.0
+# deprecated-reference-since-9.1
 #    renamings performed in Coq's standard library;
 #    using the new names would break compatibility with earlier Coq versions.
 # deprecated-from-Coq
 #    Rocq wants "From Stdlib Require" while Coq wants "From Coq Require".
-
+# register-all
+#    Rocq 9.2 warns on inductive datatypes that recurse through list or prod
+# notation-for-abbreviation
+#    The warning and the `Abbreviation` keyword needed to fix it
+#    were both introduced in Rocq 9.2.
+# implicit-create-rewrite-hint-db
+#    The warning and the `Create Rewrite Hintdb` command needed to fix it
+#    were both introduced in Rocq 9.2.
+# deprecated-end-tac
+#    Warning introduced in Rocq 9.2, should go away in later Rocq versions
 COQCOPTS ?= \
   -w -unused-pattern-matching-variable \
   -w -deprecated-since-8.19 \
   -w -deprecated-since-8.20 \
-  -w -deprecated-from-Coq
+  -w -deprecated-reference-since-9.0 \
+  -w -deprecated-reference-since-9.1 \
+  -w -deprecated-from-Coq \
+  -w -register-all \
+  -w -notation-for-abbreviation \
+  -w -implicit-create-rewrite-hint-db \
+  -w -deprecated-end-tac
 
-cparser/Parser.vo: COQCOPTS += -w -deprecated-instance-without-locality
-MenhirLib/Interpreter.vo: COQCOPTS += -w -undeclared-scope
+# deprecated-instance-without-locality:
+#    warning introduced in 8.14
+#    triggered by Menhir-generated files, to be solved upstream in Menhir
+# deprecated-exact-proof:
+#    warning introduced in 9.2
+#    triggered by Menhir-generated files, to be solved upstream in Menhir
+
+cparser/Parser.vo: COQCOPTS += -w -deprecated-instance-without-locality -w -deprecated-exact-proof
 
 # Flocq and Menhirlib run into other renaming issues.
 # These warnings can only be addressed upstream.
 
-flocq/%.vo: COQCOPTS+=-w -deprecated-syntactic-definition -w -deprecated-since-9.0
-MenhirLib/%.vo: COQCOPTS+=-w -deprecated-syntactic-definition -w -deprecated-since-9.0
+flocq/%.vo MenhirLib/%.vo: COQCOPTS+=\
+  -w -deprecated-syntactic-definition \
+  -w -deprecated-since-9.0 \
+  -w -deprecated-since-9.1 \
+  -w -deprecated-since-9.2
 
 # For the extraction phase, we silence other warnings:
 # change-dir-deprecated:
@@ -113,11 +133,16 @@ ifneq (,$(PROFILING))
 endif
 PROFILE_ZIP ?= true
 
-COQC="$(COQBIN)coqc" -q $(COQINCLUDES) $(COQCOPTS)
-COQDEP="$(COQBIN)coqdep" $(COQINCLUDES)
-COQDOC="$(COQBIN)coqdoc"
-COQEXEC="$(COQBIN)coqtop" $(COQINCLUDES) $(COQEXTRACTOPTS) -batch -load-vernac-source
-COQCHK="$(COQBIN)coqchk" $(COQINCLUDES)
+ifeq ($(USE_ROCQ),true)
+COQCOMMAND="$(COQBIN)rocq" $(2)
+else
+COQCOMMAND="$(COQBIN)$(1)"
+endif
+
+COQC=$(call COQCOMMAND,coqc,compile) -q $(COQINCLUDES) $(COQCOPTS)
+COQDEP=$(call COQCOMMAND,coqdep,dep) $(COQINCLUDES)
+COQEXEC=$(call COQCOMMAND,coqtop,repl) $(COQINCLUDES) $(COQEXTRACTOPTS) -batch -load-vernac-source
+COQCHK=$(call COQCOMMAND,coqchk,check) $(COQINCLUDES)
 COQ2HTML=coq2html
 MENHIR=menhir
 CP=cp
@@ -311,13 +336,13 @@ latexdoc:
 
 %.vo: %.v
 	@rm -f doc/$(*F).glob
-	@echo "COQC $*.v"
+	@echo "  CROCQ $*.v"
 	@$(COQC) $*.v
 	@$(PROFILE_ZIP)
 
 %.v: %.vp tools/ndfun
 	@rm -f $*.v
-	@echo "Preprocessing $*.vp"
+	@echo "  Preprocessing $*.vp"
 	@tools/ndfun $*.vp > $*.v || { rm -f $*.v; exit 2; }
 	@chmod a-w $*.v
 
@@ -369,7 +394,7 @@ cparser/Parser.v: cparser/Parser.vy
 depend: $(GENERATED) depend1
 
 depend1: $(FILES)
-	@echo "Analyzing Coq dependencies"
+	@echo "  Analyzing Coq dependencies"
 	@$(COQDEP) $^ > .depend
 
 install:
diff --git a/MenhirLib/Interpreter.v b/MenhirLib/Interpreter.v
index 6ae6edaec..c125ca548 100644
--- a/MenhirLib/Interpreter.v
+++ b/MenhirLib/Interpreter.v
@@ -82,8 +82,8 @@ CoInductive buffer : Type :=
   Buf_cons { buf_head : token; buf_tail : buffer }.
 
 (* Note: Coq 8.12.0 wants a Declare Scope command,
-   but this breaks compatibility with Coq < 8.10.
-   Declare Scope buffer_scope. *)
+   but this breaks compatibility with Coq < 8.10. *)
+Declare Scope buffer_scope.
 Delimit Scope buffer_scope with buf.
 Bind Scope buffer_scope with buffer.
 
diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index 207e8080d..16890e0de 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -37,18 +37,18 @@ Let tge := Genv.globalenv tprog.
 
 Lemma symbols_preserved:
   forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
-Proof (Genv.find_symbol_match TRANSF).
+Proof. exact (Genv.find_symbol_match TRANSF). Qed.
 
 Lemma senv_preserved:
   Senv.equiv ge tge.
-Proof (Genv.senv_match TRANSF).
+Proof. exact (Genv.senv_match TRANSF). Qed.
 
 Lemma functions_translated:
   forall b f,
   Genv.find_funct_ptr ge b = Some f ->
   exists tf,
   Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf.
-Proof (Genv.find_funct_ptr_transf_partial TRANSF).
+Proof. exact (Genv.find_funct_ptr_transf_partial TRANSF). Qed.
 
 Lemma functions_transl:
   forall fb f tf,
diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v
index 2e731cea3..cf7d97a7c 100644
--- a/arm/Asmgenproof.v
+++ b/arm/Asmgenproof.v
@@ -39,18 +39,18 @@ Let tge := Genv.globalenv tprog.
 
 Lemma symbols_preserved:
   forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
-Proof (Genv.find_symbol_match TRANSF).
+Proof. exact (Genv.find_symbol_match TRANSF). Qed.
 
 Lemma senv_preserved:
   Senv.equiv ge tge.
-Proof (Genv.senv_match TRANSF).
+Proof. exact (Genv.senv_match TRANSF). Qed.
 
 Lemma functions_translated:
   forall b f,
   Genv.find_funct_ptr ge b = Some f ->
   exists tf,
   Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf.
-Proof (Genv.find_funct_ptr_transf_partial TRANSF).
+Proof. exact (Genv.find_funct_ptr_transf_partial TRANSF). Qed.
 
 Lemma functions_transl:
   forall fb f tf,
diff --git a/backend/Allocation.v b/backend/Allocation.v
index 07fb61559..e7c28b916 100644
--- a/backend/Allocation.v
+++ b/backend/Allocation.v
@@ -407,11 +407,11 @@ Module OrderedEquation <: OrderedType.
     (OrderedLoc.lt (eloc x) (eloc y) \/ (eloc x = eloc y /\
     OrderedEqKind.lt (ekind x) (ekind y)))).
   Lemma eq_refl : forall x : t, eq x x.
-  Proof (@eq_refl t).
+  Proof. exact (@eq_refl t). Qed.
   Lemma eq_sym : forall x y : t, eq x y -> eq y x.
-  Proof (@eq_sym t).
+  Proof. exact (@eq_sym t). Qed.
   Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
-  Proof (@eq_trans t).
+  Proof. exact (@eq_trans t). Qed.
   Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
   Proof.
     unfold lt; intros.
@@ -469,11 +469,11 @@ Module OrderedEquation' <: OrderedType.
     (Plt (ereg x) (ereg y) \/ (ereg x = ereg y /\
     OrderedEqKind.lt (ekind x) (ekind y)))).
   Lemma eq_refl : forall x : t, eq x x.
-  Proof (@eq_refl t).
+  Proof. exact (@eq_refl t). Qed.
   Lemma eq_sym : forall x y : t, eq x y -> eq y x.
-  Proof (@eq_sym t).
+  Proof. exact (@eq_sym t). Qed.
   Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
-  Proof (@eq_trans t).
+  Proof. exact (@eq_trans t). Qed.
   Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
   Proof.
     unfold lt; intros.
diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index 43fdb4076..93f2dcb05 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -1790,25 +1790,25 @@ Let tge := Genv.globalenv tprog.
 
 Lemma symbols_preserved:
   forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
-Proof (Genv.find_symbol_match TRANSF).
+Proof. exact (Genv.find_symbol_match TRANSF). Qed.
 
 Lemma senv_preserved:
   Senv.equiv ge tge.
-Proof (Genv.senv_match TRANSF).
+Proof. exact (Genv.senv_match TRANSF). Qed.
 
 Lemma functions_translated:
   forall (v: val) (f: RTL.fundef),
   Genv.find_funct ge v = Some f ->
   exists tf,
   Genv.find_funct tge v = Some tf /\ transf_fundef f = OK tf.
-Proof (Genv.find_funct_transf_partial TRANSF).
+Proof. exact (Genv.find_funct_transf_partial TRANSF). Qed.
 
 Lemma function_ptr_translated:
   forall (b: block) (f: RTL.fundef),
   Genv.find_funct_ptr ge b = Some f ->
   exists tf,
   Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf.
-Proof (Genv.find_funct_ptr_transf_partial TRANSF).
+Proof. exact (Genv.find_funct_ptr_transf_partial TRANSF). Qed.
 
 Lemma sig_function_translated:
   forall f tf,
diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v
index 85cee14f3..0983dd1c1 100644
--- a/backend/Asmgenproof0.v
+++ b/backend/Asmgenproof0.v
@@ -31,6 +31,7 @@ Require Import Conventions.
 
 (** * Processor registers and register states *)
 
+Create HintDb asmgen.
 Global Hint Extern 2 (_ <> _) => congruence: asmgen.
 
 Lemma ireg_of_eq:
@@ -746,6 +747,7 @@ Qed.
 Definition nolabel (i: instruction) :=
   match i with Plabel _ => False | _ => True end.
 
+Create HintDb labels.
 Global Hint Extern 1 (nolabel _) => exact I : labels.
 
 Lemma tail_nolabel_cons:
diff --git a/backend/CSEdomain.v b/backend/CSEdomain.v
index 183d5c85d..4a50d6dd0 100644
--- a/backend/CSEdomain.v
+++ b/backend/CSEdomain.v
@@ -117,6 +117,7 @@ Record wf_numbering (n: numbering) : Prop := {
       In r (PMap.get v n.(num_val)) -> PTree.get r n.(num_reg) = Some v
 }.
 
+Create HintDb cse.
 Global Hint Resolve wf_num_eqs wf_num_reg wf_num_val: cse.
 
 (** Satisfiability of numberings.  A numbering holds in a concrete
diff --git a/backend/CSEproof.v b/backend/CSEproof.v
index cf1635ec1..9cd5d63b9 100644
--- a/backend/CSEproof.v
+++ b/backend/CSEproof.v
@@ -1079,11 +1079,11 @@ Let tge := Genv.globalenv tprog.
 
 Lemma symbols_preserved:
   forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
-Proof (Genv.find_symbol_match TRANSF).
+Proof. exact (Genv.find_symbol_match TRANSF). Qed.
 
 Lemma senv_preserved:
   Senv.equiv ge tge.
-Proof (Genv.senv_match TRANSF).
+Proof. exact (Genv.senv_match TRANSF). Qed.
 
 Lemma functions_translated:
   forall (v: val) (f: RTL.fundef),
@@ -1091,7 +1091,7 @@ Lemma functions_translated:
   exists cu tf, Genv.find_funct tge v = Some tf
              /\ transf_fundef (prog_defmap cu) (romem_for cu) f = OK tf
              /\ linkorder cu prog.
-Proof (Genv.find_funct_match TRANSF).
+Proof. exact (Genv.find_funct_match TRANSF). Qed.
 
 Lemma funct_ptr_translated:
   forall (b: block) (f: RTL.fundef),
@@ -1099,7 +1099,7 @@ Lemma funct_ptr_translated:
   exists cu tf, Genv.find_funct_ptr tge b = Some tf
              /\ transf_fundef (prog_defmap cu) (romem_for cu) f = OK tf
              /\ linkorder cu prog.
-Proof (Genv.find_funct_ptr_match TRANSF).
+Proof. exact (Genv.find_funct_ptr_match TRANSF). Qed.
 
 Lemma sig_preserved:
   forall dm rm f tf, transf_fundef dm rm f = OK tf -> funsig tf = funsig f.
diff --git a/backend/CleanupLabelsproof.v b/backend/CleanupLabelsproof.v
index bfb872220..a5631d89b 100644
--- a/backend/CleanupLabelsproof.v
+++ b/backend/CleanupLabelsproof.v
@@ -40,23 +40,23 @@ Let tge := Genv.globalenv tprog.
 Lemma symbols_preserved:
   forall id,
   Genv.find_symbol tge id = Genv.find_symbol ge id.
-Proof (Genv.find_symbol_transf TRANSL).
+Proof. exact (Genv.find_symbol_transf TRANSL). Qed.
 
 Lemma senv_preserved:
   Senv.equiv ge tge.
-Proof (Genv.senv_transf TRANSL).
+Proof. exact (Genv.senv_transf TRANSL). Qed.
 
 Lemma functions_translated:
   forall v f,
   Genv.find_funct ge v = Some f ->
   Genv.find_funct tge v = Some (transf_fundef f).
-Proof (Genv.find_funct_transf TRANSL).
+Proof. exact (Genv.find_funct_transf TRANSL). Qed.
 
 Lemma function_ptr_translated:
   forall v f,
   Genv.find_funct_ptr ge v = Some f ->
   Genv.find_funct_ptr tge v = Some (transf_fundef f).
-Proof (Genv.find_funct_ptr_transf TRANSL).
+Proof. exact (Genv.find_funct_ptr_transf TRANSL). Qed.
 
 Lemma sig_function_translated:
   forall f,
diff --git a/backend/Cminor.v b/backend/Cminor.v
index 6cd61da3c..779ca20fd 100644
--- a/backend/Cminor.v
+++ b/backend/Cminor.v
@@ -1152,7 +1152,7 @@ Lemma eval_funcall_steps:
    is_call_cont k ->
    star step ge (Callstate fd args k m)
               t (Returnstate res k m').
-Proof (proj1 eval_funcall_exec_stmt_steps).
+Proof. exact (proj1 eval_funcall_exec_stmt_steps). Qed.
 
 Lemma exec_stmt_steps:
    forall f sp e m s t e' m' out,
@@ -1161,7 +1161,7 @@ Lemma exec_stmt_steps:
    exists S,
    star step ge (State f s k sp e m) t S
    /\ outcome_state_match sp e' m' f k out S.
-Proof (proj2 eval_funcall_exec_stmt_steps).
+Proof. exact (proj2 eval_funcall_exec_stmt_steps). Qed.
 
 Lemma evalinf_funcall_forever:
   forall m fd args T k,
diff --git a/backend/CminorSel.v b/backend/CminorSel.v
index 660e61942..2ff4b0454 100644
--- a/backend/CminorSel.v
+++ b/backend/CminorSel.v
@@ -459,6 +459,7 @@ Inductive final_state: state -> int -> Prop :=
 Definition semantics (p: program) :=
   Semantics step (initial_state p) final_state (Genv.globalenv p).
 
+Create HintDb evalexpr.
 Global Hint Constructors eval_expr eval_exprlist eval_condexpr: evalexpr.
 
 (** * Lifting of let-bound variables *)
diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v
index 106eb4668..330490f6b 100644
--- a/backend/Constpropproof.v
+++ b/backend/Constpropproof.v
@@ -44,11 +44,11 @@ Let tge := Genv.globalenv tprog.
 
 Lemma symbols_preserved:
   forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
-Proof (Genv.find_symbol_match TRANSL).
+Proof. exact (Genv.find_symbol_match TRANSL). Qed.
 
 Lemma senv_preserved:
   Senv.equiv ge tge.
-Proof (Genv.senv_match TRANSL).
+Proof. exact (Genv.senv_match TRANSL). Qed.
 
 Lemma functions_translated:
   forall (v: val) (f: fundef),
diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v
index 5cda3991b..b779c7351 100644
--- a/backend/Deadcodeproof.v
+++ b/backend/Deadcodeproof.v
@@ -413,25 +413,25 @@ Let tge := Genv.globalenv tprog.
 
 Lemma symbols_preserved:
   forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
-Proof (Genv.find_symbol_match TRANSF).
+Proof. exact (Genv.find_symbol_match TRANSF). Qed.
 
 Lemma senv_preserved:
   Senv.equiv ge tge.
-Proof (Genv.senv_match TRANSF).
+Proof. exact (Genv.senv_match TRANSF). Qed.
 
 Lemma functions_translated:
   forall (v: val) (f: RTL.fundef),
   Genv.find_funct ge v = Some f ->
   exists cu tf,
   Genv.find_funct tge v = Some tf /\ transf_fundef (prog_defmap cu) (romem_for cu) f = OK tf /\ linkorder cu prog.
-Proof (Genv.find_funct_match TRANSF).
+Proof. exact (Genv.find_funct_match TRANSF). Qed.
 
 Lemma function_ptr_translated:
   forall (b: block) (f: RTL.fundef),
   Genv.find_funct_ptr ge b = Some f ->
   exists cu tf,
   Genv.find_funct_ptr tge b = Some tf /\ transf_fundef (prog_defmap cu) (romem_for cu) f = OK tf /\ linkorder cu prog.
-Proof (Genv.find_funct_ptr_match TRANSF).
+Proof. exact (Genv.find_funct_ptr_match TRANSF). Qed.
 
 Lemma sig_function_translated:
   forall dm rm f tf,
diff --git a/backend/Debugvarproof.v b/backend/Debugvarproof.v
index d31c63ec7..bd0f6d957 100644
--- a/backend/Debugvarproof.v
+++ b/backend/Debugvarproof.v
@@ -296,25 +296,25 @@ Let tge := Genv.globalenv tprog.
 
 Lemma symbols_preserved:
   forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
-Proof (Genv.find_symbol_match TRANSF).
+Proof. exact (Genv.find_symbol_match TRANSF). Qed.
 
 Lemma senv_preserved:
   Senv.equiv ge tge.
-Proof (Genv.senv_match TRANSF).
+Proof. exact (Genv.senv_match TRANSF). Qed.
 
 Lemma functions_translated:
   forall (v: val) (f: fundef),
   Genv.find_funct ge v = Some f ->
   exists tf,
   Genv.find_funct tge v = Some tf /\ transf_fundef f = OK tf.
-Proof (Genv.find_funct_transf_partial TRANSF).
+Proof. exact (Genv.find_funct_transf_partial TRANSF). Qed.
 
 Lemma function_ptr_translated:
   forall (b: block) (f: fundef),
   Genv.find_funct_ptr ge b = Some f ->
   exists tf,
   Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf.
-Proof (Genv.find_funct_ptr_transf_partial TRANSF).
+Proof. exact (Genv.find_funct_ptr_transf_partial TRANSF). Qed.
 
 Lemma sig_preserved:
   forall f tf,
diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v
index a27c4e543..c28b57e45 100644
--- a/backend/Inliningproof.v
+++ b/backend/Inliningproof.v
@@ -36,23 +36,23 @@ Let tge := Genv.globalenv tprog.
 
 Lemma symbols_preserved:
   forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
-Proof (Genv.find_symbol_match TRANSF).
+Proof. exact (Genv.find_symbol_match TRANSF). Qed.
 
 Lemma senv_preserved:
   Senv.equiv ge tge.
-Proof (Genv.senv_match TRANSF).
+Proof. exact (Genv.senv_match TRANSF). Qed.
 
 Lemma functions_translated:
   forall (v: val) (f: fundef),
   Genv.find_funct ge v = Some f ->
   exists cu f', Genv.find_funct tge v = Some f' /\ transf_fundef (funenv_program cu) f = OK f' /\ linkorder cu prog.
-Proof (Genv.find_funct_match TRANSF).
+Proof. exact (Genv.find_funct_match TRANSF). Qed.
 
 Lemma function_ptr_translated:
   forall (b: block) (f: fundef),
   Genv.find_funct_ptr ge b = Some f ->
   exists cu f', Genv.find_funct_ptr tge b = Some f' /\ transf_fundef (funenv_program cu) f = OK f' /\ linkorder cu prog.
-Proof (Genv.find_funct_ptr_match TRANSF).
+Proof. exact (Genv.find_funct_ptr_match TRANSF). Qed.
 
 Lemma sig_function_translated:
   forall cu f f', transf_fundef (funenv_program cu) f = OK f' -> funsig f' = funsig f.
diff --git a/backend/Kildall.v b/backend/Kildall.v
index 8e712c055..67568ae52 100644
--- a/backend/Kildall.v
+++ b/backend/Kildall.v
@@ -1613,11 +1613,11 @@ Module NodeSetBackward <: NODE_SET.
 
   Lemma empty_spec:
     forall n, ~In n empty.
-  Proof NodeSetForward.empty_spec.
+  Proof. exact NodeSetForward.empty_spec. Qed.
 
   Lemma add_spec:
     forall n n' s, In n' (add n s) <-> n = n' \/ In n' s.
-  Proof NodeSetForward.add_spec.
+  Proof. exact NodeSetForward.add_spec. Qed.
 
   Lemma pick_none:
     forall s n, pick s = None -> ~In n s.
@@ -1640,6 +1640,6 @@ Module NodeSetBackward <: NODE_SET.
   Lemma all_nodes_spec:
     forall A (code: PTree.t A) n instr,
     code!n = Some instr -> In n (all_nodes code).
-  Proof NodeSetForward.all_nodes_spec.
+  Proof. exact NodeSetForward.all_nodes_spec. Qed.
 End NodeSetBackward.
 
diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v
index e2c137801..643e320b1 100644
--- a/backend/Linearizeproof.v
+++ b/backend/Linearizeproof.v
@@ -45,23 +45,23 @@ Lemma functions_translated:
   Genv.find_funct ge v = Some f ->
   exists tf,
   Genv.find_funct tge v = Some tf /\ transf_fundef f = OK tf.
-Proof (Genv.find_funct_transf_partial TRANSF).
+Proof. exact (Genv.find_funct_transf_partial TRANSF). Qed.
 
 Lemma function_ptr_translated:
   forall v f,
   Genv.find_funct_ptr ge v = Some f ->
   exists tf,
   Genv.find_funct_ptr tge v = Some tf /\ transf_fundef f = OK tf.
-Proof (Genv.find_funct_ptr_transf_partial TRANSF).
+Proof. exact (Genv.find_funct_ptr_transf_partial TRANSF). Qed.
 
 Lemma symbols_preserved:
   forall id,
   Genv.find_symbol tge id = Genv.find_symbol ge id.
-Proof (Genv.find_symbol_transf_partial TRANSF).
+Proof. exact (Genv.find_symbol_transf_partial TRANSF). Qed.
 
 Lemma senv_preserved:
   Senv.equiv ge tge.
-Proof (Genv.senv_transf_partial TRANSF).
+Proof. exact (Genv.senv_transf_partial TRANSF). Qed.
 
 Lemma sig_preserved:
   forall f tf,
diff --git a/backend/Locations.v b/backend/Locations.v
index 00d8c5a99..6eac6716b 100644
--- a/backend/Locations.v
+++ b/backend/Locations.v
@@ -19,6 +19,8 @@ Require Import AST Values.
 Require Archi.
 Require Export Machregs.
 
+Create HintDb locs.
+
 (** * Representation of locations *)
 
 (** A location is either a processor register or (an abstract designation of)
@@ -469,11 +471,11 @@ Module OrderedLoc <: OrderedType.
         (ofs1 < ofs2 \/ (ofs1 = ofs2 /\ OrderedTyp.lt ty1 ty2)))
     end.
   Lemma eq_refl : forall x : t, eq x x.
-  Proof (@eq_refl t).
+  Proof. exact (@eq_refl t). Qed.
   Lemma eq_sym : forall x y : t, eq x y -> eq y x.
-  Proof (@eq_sym t).
+  Proof. exact (@eq_sym t). Qed.
   Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
-  Proof (@eq_trans t).
+  Proof. exact (@eq_trans t). Qed.
   Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
   Proof.
     unfold lt; intros.
diff --git a/backend/NeedDomain.v b/backend/NeedDomain.v
index 8d95be299..2e617aea7 100644
--- a/backend/NeedDomain.v
+++ b/backend/NeedDomain.v
@@ -85,6 +85,7 @@ Proof.
   intros. simpl in H. auto.
 Qed.
 
+Create HintDb na.
 Global Hint Resolve vagree_same vagree_lessdef lessdef_vagree: na.
 
 Inductive vagree_list: list val -> list val -> list nval -> Prop :=
@@ -753,19 +754,19 @@ Lemma and_sound:
   forall v1 w1 v2 w2 x,
   vagree v1 w1 (bitwise x) -> vagree v2 w2 (bitwise x) ->
   vagree (Val.and v1 v2) (Val.and w1 w2) x.
-Proof (vagree_bitwise_binop Int.and (iagree_bitwise_binop andb Int.and Int.bits_and)).
+Proof. exact (vagree_bitwise_binop Int.and (iagree_bitwise_binop andb Int.and Int.bits_and)). Qed.
 
 Lemma or_sound:
   forall v1 w1 v2 w2 x,
   vagree v1 w1 (bitwise x) -> vagree v2 w2 (bitwise x) ->
   vagree (Val.or v1 v2) (Val.or w1 w2) x.
-Proof (vagree_bitwise_binop Int.or (iagree_bitwise_binop orb Int.or Int.bits_or)).
+Proof. exact (vagree_bitwise_binop Int.or (iagree_bitwise_binop orb Int.or Int.bits_or)). Qed.
 
 Lemma xor_sound:
   forall v1 w1 v2 w2 x,
   vagree v1 w1 (bitwise x) -> vagree v2 w2 (bitwise x) ->
   vagree (Val.xor v1 v2) (Val.xor w1 w2) x.
-Proof (vagree_bitwise_binop Int.xor (iagree_bitwise_binop xorb Int.xor Int.bits_xor)).
+Proof. exact (vagree_bitwise_binop Int.xor (iagree_bitwise_binop xorb Int.xor Int.bits_xor)). Qed.
 
 Lemma notint_sound:
   forall v w x,
@@ -797,19 +798,19 @@ Lemma andl_sound:
   forall v1 w1 v2 w2 x,
   vagree v1 w1 (bitwise x) -> vagree v2 w2 (bitwise x) ->
   vagree (Val.andl v1 v2) (Val.andl w1 w2) x.
-Proof (vagree_bitwise64_binop Int64.and (lagree_bitwise_binop andb Int64.and Int64.bits_and)).
+Proof. exact (vagree_bitwise64_binop Int64.and (lagree_bitwise_binop andb Int64.and Int64.bits_and)). Qed.
 
 Lemma orl_sound:
   forall v1 w1 v2 w2 x,
   vagree v1 w1 (bitwise x) -> vagree v2 w2 (bitwise x) ->
   vagree (Val.orl v1 v2) (Val.orl w1 w2) x.
-Proof (vagree_bitwise64_binop Int64.or (lagree_bitwise_binop orb Int64.or Int64.bits_or)).
+Proof. exact (vagree_bitwise64_binop Int64.or (lagree_bitwise_binop orb Int64.or Int64.bits_or)). Qed.
 
 Lemma xorl_sound:
   forall v1 w1 v2 w2 x,
   vagree v1 w1 (bitwise x) -> vagree v2 w2 (bitwise x) ->
   vagree (Val.xorl v1 v2) (Val.xorl w1 w2) x.
-Proof (vagree_bitwise64_binop Int64.xor (lagree_bitwise_binop xorb Int64.xor Int64.bits_xor)).
+Proof. exact (vagree_bitwise64_binop Int64.xor (lagree_bitwise_binop xorb Int64.xor Int64.bits_xor)). Qed.
 
 Lemma notl_sound:
   forall v w x,
@@ -1825,9 +1826,9 @@ Module NVal <: SEMILATTICE.
   Proof. intros. constructor. Qed.
   Definition lub := nlub.
   Lemma ge_lub_left: forall x y, ge (lub x y) x.
-  Proof nge_lub_l.
+  Proof. exact nge_lub_l. Qed.
   Lemma ge_lub_right: forall x y, ge (lub x y) y.
-  Proof nge_lub_r.
+  Proof. exact nge_lub_r. Qed.
 End NVal.
 
 Module NE := LPMap1(NVal).
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index f0dd2604b..5938aa536 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -372,24 +372,27 @@ Let tge : RTL.genv := Genv.globalenv tprog.
 
 Lemma symbols_preserved:
   forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
-Proof
-  (Genv.find_symbol_transf_partial TRANSL).
+Proof.
+  exact (Genv.find_symbol_transf_partial TRANSL).
+Qed.
 
 Lemma function_ptr_translated:
   forall (b: block) (f: CminorSel.fundef),
   Genv.find_funct_ptr ge b = Some f ->
   exists tf,
   Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = OK tf.
-Proof
-  (Genv.find_funct_ptr_transf_partial TRANSL).
+Proof.
+  exact (Genv.find_funct_ptr_transf_partial TRANSL).
+Qed.
 
 Lemma functions_translated:
   forall (v: val) (f: CminorSel.fundef),
   Genv.find_funct ge v = Some f ->
   exists tf,
   Genv.find_funct tge v = Some tf /\ transl_fundef f = OK tf.
-Proof
-  (Genv.find_funct_transf_partial TRANSL).
+Proof.
+  exact (Genv.find_funct_transf_partial TRANSL).
+Qed.
 
 Lemma sig_transl_function:
   forall (f: CminorSel.fundef) (tf: RTL.fundef),
@@ -407,8 +410,9 @@ Qed.
 
 Lemma senv_preserved:
   Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge).
-Proof
-  (Genv.senv_transf_partial TRANSL).
+Proof.
+  exact (Genv.senv_transf_partial TRANSL).
+Qed.
 
 (** Correctness of the code generated by [add_move]. *)
 
@@ -872,8 +876,8 @@ Theorem transl_expr_correct:
   forall le a v,
   eval_expr ge sp e m le a v ->
   transl_expr_prop le a v.
-Proof
-  (eval_expr_ind3 ge sp e m
+Proof.
+  exact (eval_expr_ind3 ge sp e m
      transl_expr_prop
      transl_exprlist_prop
      transl_condexpr_prop
@@ -890,13 +894,14 @@ Proof
      transl_condexpr_CEcond_correct
      transl_condexpr_CEcondition_correct
      transl_condexpr_CElet_correct).
+Qed.
 
 Theorem transl_exprlist_correct:
   forall le a v,
   eval_exprlist ge sp e m le a v ->
   transl_exprlist_prop le a v.
-Proof
-  (eval_exprlist_ind3 ge sp e m
+Proof.
+  exact (eval_exprlist_ind3 ge sp e m
      transl_expr_prop
      transl_exprlist_prop
      transl_condexpr_prop
@@ -913,13 +918,14 @@ Proof
      transl_condexpr_CEcond_correct
      transl_condexpr_CEcondition_correct
      transl_condexpr_CElet_correct).
+Qed.
 
 Theorem transl_condexpr_correct:
   forall le a v,
   eval_condexpr ge sp e m le a v ->
   transl_condexpr_prop le a v.
-Proof
-  (eval_condexpr_ind3 ge sp e m
+Proof.
+  exact (eval_condexpr_ind3 ge sp e m
      transl_expr_prop
      transl_exprlist_prop
      transl_condexpr_prop
@@ -936,6 +942,7 @@ Proof
      transl_condexpr_CEcond_correct
      transl_condexpr_CEcondition_correct
      transl_condexpr_CElet_correct).
+Qed.
 
 (** Exit expressions. *)
 
diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v
index 3f9e3195f..1c4612de1 100644
--- a/backend/RTLgenspec.v
+++ b/backend/RTLgenspec.v
@@ -128,6 +128,7 @@ Ltac monadInv H :=
 
 (** * Monotonicity properties of the state *)
 
+Create HintDb rtlg.
 Global Hint Resolve state_incr_refl: rtlg.
 
 Lemma instr_at_incr:
diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index 9db5c4f4d..fe5e16b94 100644
--- a/backend/RTLtyping.v
+++ b/backend/RTLtyping.v
@@ -707,7 +707,7 @@ Proof.
   rewrite check_successor_complete by auto. simpl.
   exists (match ef with EF_annot _ _ _ | EF_debug _ _ _ => e3 | _ => e2 end); split.
   rewrite H1 in C, E.
-  destruct ef; try (rewrite <- H0; rewrite A); simpl; auto.
+  destruct ef; auto; rewrite <- H0, A; simpl; auto.
   destruct ef; auto.
 - (* cond *)
   exploit S.set_list_complete. eauto. eauto. intros [e1 [A B]].
diff --git a/backend/Renumberproof.v b/backend/Renumberproof.v
index 7cda94257..dd15b98ba 100644
--- a/backend/Renumberproof.v
+++ b/backend/Renumberproof.v
@@ -37,22 +37,22 @@ Lemma functions_translated:
   forall v f,
   Genv.find_funct ge v = Some f ->
   Genv.find_funct tge v = Some (transf_fundef f).
-Proof (Genv.find_funct_transf TRANSL).
+Proof. exact (Genv.find_funct_transf TRANSL). Qed.
 
 Lemma function_ptr_translated:
   forall v f,
   Genv.find_funct_ptr ge v = Some f ->
   Genv.find_funct_ptr tge v = Some (transf_fundef f).
-Proof (Genv.find_funct_ptr_transf TRANSL).
+Proof. exact (Genv.find_funct_ptr_transf TRANSL). Qed.
 
 Lemma symbols_preserved:
   forall id,
   Genv.find_symbol tge id = Genv.find_symbol ge id.
-Proof (Genv.find_symbol_transf TRANSL).
+Proof. exact (Genv.find_symbol_transf TRANSL). Qed.
 
 Lemma senv_preserved:
   Senv.equiv ge tge.
-Proof (Genv.senv_transf TRANSL).
+Proof. exact (Genv.senv_transf TRANSL). Qed.
 
 Lemma sig_preserved:
   forall f, funsig (transf_fundef f) = funsig f.
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index 392044fec..d7c1bdc6d 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -132,17 +132,17 @@ Qed.
 
 Lemma symbols_preserved:
   forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
-Proof (Genv.find_symbol_match TRANSF).
+Proof. exact (Genv.find_symbol_match TRANSF). Qed.
 
 Lemma senv_preserved:
   Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge).
-Proof (Genv.senv_match TRANSF).
+Proof. exact (Genv.senv_match TRANSF). Qed.
 
 Lemma function_ptr_translated:
   forall (b: block) (f: Cminor.fundef),
   Genv.find_funct_ptr ge b = Some f ->
   exists cu tf, Genv.find_funct_ptr tge b = Some tf /\ match_fundef cu f tf /\ linkorder cu prog.
-Proof (Genv.find_funct_ptr_match TRANSF).
+Proof. exact (Genv.find_funct_ptr_match TRANSF). Qed.
 
 Lemma functions_translated:
   forall (v v': val) (f: Cminor.fundef),
diff --git a/backend/SplitLongproof.v b/backend/SplitLongproof.v
index 1a8c829a7..3eb766c6a 100644
--- a/backend/SplitLongproof.v
+++ b/backend/SplitLongproof.v
@@ -141,6 +141,12 @@ Ltac EvalOp :=
   | _ => idtac
   end.
 
+Ltac UseUndef :=
+  match goal with
+  | [ H: ?x = Vundef |- Val.lessdef ?x ?y ] => rewrite H; auto
+  | _ => idtac
+  end.
+
 Lemma eval_splitlong:
   forall le a f v sem,
   (forall le a b x y,
@@ -157,14 +163,14 @@ Proof.
 - InvEval; subst.
   exploit EXEC. eexact H2. eexact H3. intros [v' [A B]].
   exists v'; split. auto.
-  destruct v1; simpl in *; try (rewrite UNDEF; auto).
-  destruct v0; simpl in *; try (rewrite UNDEF; auto).
+  destruct v1; simpl in *; UseUndef.
+  destruct v0; simpl in *; UseUndef.
   erewrite B; eauto.
 - exploit (EXEC (v :: le) (Eop Ohighlong (Eletvar 0 ::: Enil)) (Eop Olowlong (Eletvar 0 ::: Enil))).
   EvalOp. EvalOp.
   intros [v' [A B]].
   exists v'; split. econstructor; eauto.
-  destruct v; try (rewrite UNDEF; auto). erewrite B; simpl; eauto. rewrite Int64.ofwords_recompose. auto.
+  destruct v; UseUndef. erewrite B; simpl; eauto. rewrite Int64.ofwords_recompose. auto.
 Qed.
 
 Lemma eval_splitlong_strict:
@@ -205,10 +211,10 @@ Proof.
 - InvEval; subst.
   exploit (EXEC le h1 l1 h2 l2); eauto. intros [v [A B]].
   exists v; split; auto.
-  destruct v1; simpl in *; try (rewrite UNDEF; auto).
-  destruct v0; try (rewrite UNDEF; auto).
-  destruct v2; simpl in *; try (rewrite UNDEF; auto).
-  destruct v3; try (rewrite UNDEF; auto).
+  destruct v1; simpl in *; UseUndef.
+  destruct v0; UseUndef.
+  destruct v2; simpl in *; UseUndef.
+  destruct v3; UseUndef.
   erewrite B; eauto.
 - InvEval; subst.
   exploit (EXEC (vb :: le) (lift h1) (lift l1)
@@ -217,9 +223,9 @@ Proof.
   intros [v [A B]].
   exists v; split.
   econstructor; eauto.
-  destruct v1; simpl in *; try (rewrite UNDEF; auto).
-  destruct v0; try (rewrite UNDEF; auto).
-  destruct vb; try (rewrite UNDEF; auto).
+  destruct v1; simpl in *; UseUndef.
+  destruct v0; UseUndef.
+  destruct vb; UseUndef.
   erewrite B; simpl; eauto. rewrite Int64.ofwords_recompose. auto.
 - InvEval; subst.
   exploit (EXEC (va :: le)
@@ -229,9 +235,9 @@ Proof.
   intros [v [A B]].
   exists v; split.
   econstructor; eauto.
-  destruct va; try (rewrite UNDEF; auto).
-  destruct v1; simpl in *; try (rewrite UNDEF; auto).
-  destruct v0; try (rewrite UNDEF; auto).
+  destruct va; UseUndef.
+  destruct v1; simpl in *; UseUndef.
+  destruct v0; UseUndef.
   erewrite B; simpl; eauto. rewrite Int64.ofwords_recompose. auto.
 - exploit (EXEC (vb :: va :: le)
                 (Eop Ohighlong (Eletvar 1 ::: Enil)) (Eop Olowlong (Eletvar 1 ::: Enil))
@@ -239,7 +245,7 @@ Proof.
   EvalOp. EvalOp. EvalOp. EvalOp.
   intros [v [A B]].
   exists v; split. EvalOp.
-  destruct va; try (rewrite UNDEF; auto); destruct vb; try (rewrite UNDEF; auto).
+  destruct va; UseUndef; destruct vb; UseUndef.
   erewrite B; simpl; eauto. rewrite ! Int64.ofwords_recompose; auto.
 Qed.
 
@@ -322,7 +328,7 @@ Proof.
 Qed.
 
 Theorem eval_intoflong: unary_constructor_sound intoflong Val.loword.
-Proof eval_lowlong.
+Proof. exact eval_lowlong. Qed.
 
 Theorem eval_longofintu: unary_constructor_sound longofintu Val.longofintu.
 Proof.
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index 2a25c6f27..2d9de77b7 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -596,6 +596,7 @@ Proof.
   auto. constructor; auto using agree_reg.
 Qed.
 
+Create HintDb stacking.
 Hint Resolve agree_reg agree_reglist: stacking.
 
 (** Preservation under assignments of machine registers. *)
@@ -1570,25 +1571,25 @@ Qed.
 
 Lemma symbols_preserved:
   forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
-Proof (Genv.find_symbol_match TRANSF).
+Proof. exact (Genv.find_symbol_match TRANSF). Qed.
 
 Lemma senv_preserved:
   Senv.equiv ge tge.
-Proof (Genv.senv_match TRANSF).
+Proof. exact (Genv.senv_match TRANSF). Qed.
 
 Lemma functions_translated:
   forall v f,
   Genv.find_funct ge v = Some f ->
   exists tf,
   Genv.find_funct tge v = Some tf /\ transf_fundef f = OK tf.
-Proof (Genv.find_funct_transf_partial TRANSF).
+Proof. exact (Genv.find_funct_transf_partial TRANSF). Qed.
 
 Lemma function_ptr_translated:
   forall b f,
   Genv.find_funct_ptr ge b = Some f ->
   exists tf,
   Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf.
-Proof (Genv.find_funct_ptr_transf_partial TRANSF).
+Proof. exact (Genv.find_funct_ptr_transf_partial TRANSF). Qed.
 
 Lemma sig_preserved:
   forall f tf, transf_fundef f = OK tf -> Mach.funsig tf = Linear.funsig f.
diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v
index fa2c91ec6..282f19916 100644
--- a/backend/Tailcallproof.v
+++ b/backend/Tailcallproof.v
@@ -219,23 +219,23 @@ Let tge := Genv.globalenv tprog.
 
 Lemma symbols_preserved:
   forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
-Proof (Genv.find_symbol_transf TRANSL).
+Proof. exact (Genv.find_symbol_transf TRANSL). Qed.
 
 Lemma functions_translated:
   forall (v: val) (f: RTL.fundef),
   Genv.find_funct ge v = Some f ->
   Genv.find_funct tge v = Some (transf_fundef f).
-Proof (Genv.find_funct_transf TRANSL).
+Proof. exact (Genv.find_funct_transf TRANSL). Qed.
 
 Lemma funct_ptr_translated:
   forall (b: block) (f: RTL.fundef),
   Genv.find_funct_ptr ge b = Some f ->
   Genv.find_funct_ptr tge b = Some (transf_fundef f).
-Proof (Genv.find_funct_ptr_transf TRANSL).
+Proof. exact (Genv.find_funct_ptr_transf TRANSL). Qed.
 
 Lemma senv_preserved:
   Senv.equiv ge tge.
-Proof (Genv.senv_transf TRANSL).
+Proof. exact (Genv.senv_transf TRANSL). Qed.
 
 Lemma sig_preserved:
   forall f, funsig (transf_fundef f) = funsig f.
diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v
index c05ec20e9..40ffb1bda 100644
--- a/backend/Tunnelingproof.v
+++ b/backend/Tunnelingproof.v
@@ -269,22 +269,22 @@ Lemma functions_translated:
   forall v f,
   Genv.find_funct ge v = Some f ->
   Genv.find_funct tge v = Some (tunnel_fundef f).
-Proof (Genv.find_funct_transf TRANSL).
+Proof. exact (Genv.find_funct_transf TRANSL). Qed.
 
 Lemma function_ptr_translated:
   forall v f,
   Genv.find_funct_ptr ge v = Some f ->
   Genv.find_funct_ptr tge v = Some (tunnel_fundef f).
-Proof (Genv.find_funct_ptr_transf TRANSL).
+Proof. exact (Genv.find_funct_ptr_transf TRANSL). Qed.
 
 Lemma symbols_preserved:
   forall id,
   Genv.find_symbol tge id = Genv.find_symbol ge id.
-Proof (Genv.find_symbol_transf TRANSL).
+Proof. exact (Genv.find_symbol_transf TRANSL). Qed.
 
 Lemma senv_preserved:
   Senv.equiv ge tge.
-Proof (Genv.senv_transf TRANSL).
+Proof. exact (Genv.senv_transf TRANSL). Qed.
 
 Lemma sig_preserved:
   forall f, funsig (tunnel_fundef f) = funsig f.
diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v
index 1b0f9c081..165540777 100644
--- a/backend/ValueDomain.v
+++ b/backend/ValueDomain.v
@@ -44,6 +44,7 @@ Proof.
   elim H. apply H0; auto.
 Qed.
 
+Create HintDb va.
 Global Hint Extern 2 (_ = _) => congruence : va.
 Global Hint Extern 2 (_ <> _) => congruence : va.
 Global Hint Extern 2 (_ < _) => extlia : va.
@@ -2126,43 +2127,43 @@ Definition shll := shift_long Int64.shl'.
 
 Lemma shll_sound:
   forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.shll v w) (shll x y).
-Proof (shift_long_sound Int64.shl').
+Proof. exact (shift_long_sound Int64.shl'). Qed.
 
 Definition shrl := shift_long Int64.shr'.
 
 Lemma shrl_sound:
   forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.shrl v w) (shrl x y).
-Proof (shift_long_sound Int64.shr').
+Proof. exact (shift_long_sound Int64.shr'). Qed.
 
 Definition shrlu := shift_long Int64.shru'.
 
 Lemma shrlu_sound:
   forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.shrlu v w) (shrlu x y).
-Proof (shift_long_sound Int64.shru').
+Proof. exact (shift_long_sound Int64.shru'). Qed.
 
 Definition andl := binop_long Int64.and.
 
 Lemma andl_sound:
   forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.andl v w) (andl x y).
-Proof (binop_long_sound Int64.and).
+Proof. exact (binop_long_sound Int64.and). Qed.
 
 Definition orl := binop_long Int64.or.
 
 Lemma orl_sound:
   forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.orl v w) (orl x y).
-Proof (binop_long_sound Int64.or).
+Proof. exact (binop_long_sound Int64.or). Qed.
 
 Definition xorl := binop_long Int64.xor.
 
 Lemma xorl_sound:
   forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.xorl v w) (xorl x y).
-Proof (binop_long_sound Int64.xor).
+Proof. exact (binop_long_sound Int64.xor). Qed.
 
 Definition notl := unop_long Int64.not.
 
 Lemma notl_sound:
   forall v x, vmatch v x -> vmatch (Val.notl v) (notl x).
-Proof (unop_long_sound Int64.not).
+Proof. exact (unop_long_sound Int64.not). Qed.
 
 Definition rotate_long (sem: int64 -> int64 -> int64) (v w: aval) :=
   match v, w with
@@ -2192,19 +2193,19 @@ Definition roll := rotate_long Int64.rol.
 
 Lemma roll_sound:
   forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.roll v w) (roll x y).
-Proof (rotate_long_sound Int64.rol).
+Proof. exact (rotate_long_sound Int64.rol). Qed.
 
 Definition rorl := rotate_long Int64.ror.
 
 Lemma rorl_sound:
   forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.rorl v w) (rorl x y).
-Proof (rotate_long_sound Int64.ror).
+Proof. exact (rotate_long_sound Int64.ror). Qed.
 
 Definition negl := unop_long Int64.neg.
 
 Lemma negl_sound:
   forall v x, vmatch v x -> vmatch (Val.negl v) (negl x).
-Proof (unop_long_sound Int64.neg).
+Proof. exact (unop_long_sound Int64.neg). Qed.
 
 Definition addl (x y: aval) :=
   match x, y with
@@ -2250,19 +2251,19 @@ Definition mull := binop_long Int64.mul.
 
 Lemma mull_sound:
   forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.mull v w) (mull x y).
-Proof (binop_long_sound Int64.mul).
+Proof. exact (binop_long_sound Int64.mul). Qed.
 
 Definition mullhs := binop_long Int64.mulhs.
 
 Lemma mullhs_sound:
   forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.mullhs v w) (mullhs x y).
-Proof (binop_long_sound Int64.mulhs).
+Proof. exact (binop_long_sound Int64.mulhs). Qed.
 
 Definition mullhu := binop_long Int64.mulhu.
 
 Lemma mullhu_sound:
   forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.mullhu v w) (mullhu x y).
-Proof (binop_long_sound Int64.mulhu).
+Proof. exact (binop_long_sound Int64.mulhu). Qed.
 
 Definition divls (v w: aval) :=
   match w, v with
@@ -2387,73 +2388,73 @@ Definition negf := unop_float Float.neg.
 
 Lemma negf_sound:
   forall v x, vmatch v x -> vmatch (Val.negf v) (negf x).
-Proof (unop_float_sound Float.neg).
+Proof. exact (unop_float_sound Float.neg). Qed.
 
 Definition absf := unop_float Float.abs.
 
 Lemma absf_sound:
   forall v x, vmatch v x -> vmatch (Val.absf v) (absf x).
-Proof (unop_float_sound Float.abs).
+Proof. exact (unop_float_sound Float.abs). Qed.
 
 Definition addf := binop_float Float.add.
 
 Lemma addf_sound:
   forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.addf v w) (addf x y).
-Proof (binop_float_sound Float.add).
+Proof. exact (binop_float_sound Float.add). Qed.
 
 Definition subf := binop_float Float.sub.
 
 Lemma subf_sound:
   forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.subf v w) (subf x y).
-Proof (binop_float_sound Float.sub).
+Proof. exact (binop_float_sound Float.sub). Qed.
 
 Definition mulf := binop_float Float.mul.
 
 Lemma mulf_sound:
   forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.mulf v w) (mulf x y).
-Proof (binop_float_sound Float.mul).
+Proof. exact (binop_float_sound Float.mul). Qed.
 
 Definition divf := binop_float Float.div.
 
 Lemma divf_sound:
   forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.divf v w) (divf x y).
-Proof (binop_float_sound Float.div).
+Proof. exact (binop_float_sound Float.div). Qed.
 
 Definition negfs := unop_single Float32.neg.
 
 Lemma negfs_sound:
   forall v x, vmatch v x -> vmatch (Val.negfs v) (negfs x).
-Proof (unop_single_sound Float32.neg).
+Proof. exact (unop_single_sound Float32.neg). Qed.
 
 Definition absfs := unop_single Float32.abs.
 
 Lemma absfs_sound:
   forall v x, vmatch v x -> vmatch (Val.absfs v) (absfs x).
-Proof (unop_single_sound Float32.abs).
+Proof. exact (unop_single_sound Float32.abs). Qed.
 
 Definition addfs := binop_single Float32.add.
 
 Lemma addfs_sound:
   forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.addfs v w) (addfs x y).
-Proof (binop_single_sound Float32.add).
+Proof. exact (binop_single_sound Float32.add). Qed.
 
 Definition subfs := binop_single Float32.sub.
 
 Lemma subfs_sound:
   forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.subfs v w) (subfs x y).
-Proof (binop_single_sound Float32.sub).
+Proof. exact (binop_single_sound Float32.sub). Qed.
 
 Definition mulfs := binop_single Float32.mul.
 
 Lemma mulfs_sound:
   forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.mulfs v w) (mulfs x y).
-Proof (binop_single_sound Float32.mul).
+Proof. exact (binop_single_sound Float32.mul). Qed.
 
 Definition divfs := binop_single Float32.div.
 
 Lemma divfs_sound:
   forall v x w y, vmatch v x -> vmatch w y -> vmatch (Val.divfs v w) (divfs x y).
-Proof (binop_single_sound Float32.div).
+Proof. exact (binop_single_sound Float32.div). Qed.
 
 (** Conversions *)
 
@@ -5103,9 +5104,9 @@ Module AVal <: SEMILATTICE_WITH_TOP.
   Proof. intros. apply vge_top. Qed.
   Definition lub := vlub.
   Lemma ge_lub_left: forall x y, ge (lub x y) x.
-  Proof vge_lub_l.
+  Proof. exact vge_lub_l. Qed.
   Lemma ge_lub_right: forall x y, ge (lub x y) y.
-  Proof vge_lub_r.
+  Proof. exact vge_lub_r. Qed.
 End AVal.
 
 Module AE := LPMap(AVal).
diff --git a/cfrontend/ClightBigstep.v b/cfrontend/ClightBigstep.v
index 440466079..aba8b9c53 100644
--- a/cfrontend/ClightBigstep.v
+++ b/cfrontend/ClightBigstep.v
@@ -493,7 +493,7 @@ Lemma exec_stmt_steps:
    forall f k, exists S,
    star step_fe ge (State f s k e le m) t S
    /\ outcome_state_match e le' m' f k out S.
-Proof (proj1 exec_stmt_eval_funcall_steps).
+Proof. exact (proj1 exec_stmt_eval_funcall_steps). Qed.
 
 Lemma eval_funcall_steps:
    forall m fd args t m' res,
@@ -501,7 +501,7 @@ Lemma eval_funcall_steps:
    forall k,
    is_call_cont k ->
    star step_fe ge (Callstate fd args k m) t (Returnstate res k m').
-Proof (proj2 exec_stmt_eval_funcall_steps).
+Proof. exact (proj2 exec_stmt_eval_funcall_steps). Qed.
 
 Definition order (x y: unit) := False.
 
@@ -613,7 +613,7 @@ Definition bigstep_program_diverges := bigstep_program_diverges function_entry1.
 Definition bigstep_semantics := bigstep_semantics function_entry1.
 Theorem bigstep_semantics_sound: forall prog,
   bigstep_sound (bigstep_semantics prog) (Clight.semantics1 prog).
-Proof (bigstep_semantics_sound function_entry1).
+Proof. exact (bigstep_semantics_sound function_entry1). Qed.
 
 End Clight1.
 
@@ -630,6 +630,6 @@ Definition bigstep_program_diverges := bigstep_program_diverges function_entry2.
 Definition bigstep_semantics := bigstep_semantics function_entry2.
 Theorem bigstep_semantics_sound: forall prog,
   bigstep_sound (bigstep_semantics prog) (Clight.semantics2 prog).
-Proof (bigstep_semantics_sound function_entry2).
+Proof. exact (bigstep_semantics_sound function_entry2). Qed.
 
 End Clight2.
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index 3fb395eb7..c02b05c57 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -41,25 +41,25 @@ Let tge: genv := Genv.globalenv tprog.
 
 Lemma symbols_preserved:
   forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
-Proof (Genv.find_symbol_transf_partial TRANSL).
+Proof. exact (Genv.find_symbol_transf_partial TRANSL). Qed.
 
 Lemma senv_preserved:
   Senv.equiv ge tge.
-Proof (Genv.senv_transf_partial TRANSL).
+Proof. exact (Genv.senv_transf_partial TRANSL). Qed.
 
 Lemma function_ptr_translated:
   forall (b: block) (f: Csharpminor.fundef),
   Genv.find_funct_ptr ge b = Some f ->
   exists tf,
   Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = OK tf.
-Proof (Genv.find_funct_ptr_transf_partial TRANSL).
+Proof. exact (Genv.find_funct_ptr_transf_partial TRANSL). Qed.
 
 Lemma functions_translated:
   forall (v: val) (f: Csharpminor.fundef),
   Genv.find_funct ge v = Some f ->
   exists tf,
   Genv.find_funct tge v = Some tf /\ transl_fundef f = OK tf.
-Proof (Genv.find_funct_transf_partial TRANSL).
+Proof. exact (Genv.find_funct_transf_partial TRANSL). Qed.
 
 Lemma sig_preserved_body:
   forall f tf cenv size,
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index 84f538774..5a6c2c17d 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -262,6 +262,7 @@ Proof.
   destruct sg; econstructor; eauto.
 Qed.
 
+Create HintDb cshm.
 Hint Resolve make_intconst_correct make_floatconst_correct make_longconst_correct
              make_singleconst_correct make_singleoffloat_correct make_floatofsingle_correct
              make_floatofint_correct: cshm.
@@ -1067,23 +1068,23 @@ Let tge := Genv.globalenv tprog.
 
 Lemma symbols_preserved:
   forall s, Genv.find_symbol tge s = Genv.find_symbol ge s.
-Proof (Genv.find_symbol_match TRANSL).
+Proof. exact (Genv.find_symbol_match TRANSL). Qed.
 
 Lemma senv_preserved:
   Senv.equiv ge tge.
-Proof (Genv.senv_match TRANSL).
+Proof. exact (Genv.senv_match TRANSL). Qed.
 
 Lemma function_ptr_translated:
   forall v f,
   Genv.find_funct_ptr ge v = Some f ->
   exists cu tf, Genv.find_funct_ptr tge v = Some tf /\ match_fundef cu f tf /\ linkorder cu prog.
-Proof (Genv.find_funct_ptr_match TRANSL).
+Proof. exact (Genv.find_funct_ptr_match TRANSL). Qed.
 
 Lemma functions_translated:
   forall v f,
   Genv.find_funct ge v = Some f ->
   exists cu tf, Genv.find_funct tge v = Some tf /\ match_fundef cu f tf /\ linkorder cu prog.
-Proof (Genv.find_funct_match TRANSL).
+Proof. exact (Genv.find_funct_match TRANSL). Qed.
 
 (** * Matching between environments *)
 
@@ -1363,14 +1364,14 @@ Lemma transl_expr_correct:
    Clight.eval_expr ge e le m a v ->
    forall ta, transl_expr cunit.(prog_comp_env) a = OK ta ->
    Csharpminor.eval_expr tge te le m ta v.
-Proof (proj1 transl_expr_lvalue_correct).
+Proof. exact (proj1 transl_expr_lvalue_correct). Qed.
 
 Lemma transl_lvalue_correct:
    forall a b ofs bf,
    Clight.eval_lvalue ge e le m a b ofs bf ->
    forall ta bf', transl_lvalue cunit.(prog_comp_env) a = OK (ta, bf') ->
    bf = bf' /\ Csharpminor.eval_expr tge te le m ta (Vptr b ofs).
-Proof (proj2 transl_expr_lvalue_correct).
+Proof. exact (proj2 transl_expr_lvalue_correct). Qed.
 
 Lemma transl_arglist_correct:
   forall al tyl vl,
diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v
index 2b95fec18..0e16acb01 100644
--- a/cfrontend/Cstrategy.v
+++ b/cfrontend/Cstrategy.v
@@ -747,14 +747,14 @@ Lemma eval_simple_rvalue_steps:
   forall C, context RV RV C ->
   star Csem.step ge (ExprState f (C a) k e m)
                 E0 (ExprState f (C (Eval v (typeof a))) k e m).
-Proof (proj1 eval_simple_steps).
+Proof. exact (proj1 eval_simple_steps). Qed.
 
 Lemma eval_simple_lvalue_steps:
   forall a b ofs bf, eval_simple_lvalue e m a b ofs bf ->
   forall C, context LV RV C ->
   star Csem.step ge (ExprState f (C a) k e m)
                 E0 (ExprState f (C (Eloc b ofs bf (typeof a))) k e m).
-Proof (proj2 eval_simple_steps).
+Proof. exact (proj2 eval_simple_steps). Qed.
 
 Corollary eval_simple_rvalue_safe:
   forall C a v,
@@ -2610,7 +2610,7 @@ Lemma eval_expression_to_steps:
    eval_expression e m a t m' v ->
    forall f k,
    star step ge (ExprState f a k e m) t (ExprState f (Eval v (typeof a)) k e m').
-Proof (proj1 bigstep_to_steps).
+Proof. exact (proj1 bigstep_to_steps). Qed.
 
 Lemma eval_expr_to_steps:
    forall e m K a t m' a',
@@ -2618,7 +2618,7 @@ Lemma eval_expr_to_steps:
    forall C f k, leftcontext K RV C ->
    simple a' = true /\ typeof a' = typeof a /\
    star step ge (ExprState f (C a) k e m) t (ExprState f (C a') k e m').
-Proof (proj1 (proj2 bigstep_to_steps)).
+Proof. exact (proj1 (proj2 bigstep_to_steps)). Qed.
 
 Lemma eval_exprlist_to_steps:
    forall e m al t m' al',
@@ -2627,7 +2627,7 @@ Lemma eval_exprlist_to_steps:
    simplelist al' = true /\
    star step ge (ExprState f (C (Ecall a1 (exprlist_app al2 al) ty)) k e m)
               t (ExprState f (C (Ecall a1 (exprlist_app al2 al') ty)) k e m').
-Proof (proj1 (proj2 (proj2 bigstep_to_steps))).
+Proof. exact (proj1 (proj2 (proj2 bigstep_to_steps))). Qed.
 
 Lemma exec_stmt_to_steps:
    forall e m s t m' out,
@@ -2635,7 +2635,7 @@ Lemma exec_stmt_to_steps:
    forall f k,
    exists S,
    star step ge (State f s k e m) t S /\ outcome_state_match e m' f k out S.
-Proof (proj1 (proj2 (proj2 (proj2 bigstep_to_steps)))).
+Proof. exact (proj1 (proj2 (proj2 (proj2 bigstep_to_steps)))). Qed.
 
 Lemma eval_funcall_to_steps:
   forall m fd args t m' res,
@@ -2643,7 +2643,7 @@ Lemma eval_funcall_to_steps:
   forall k,
   is_call_cont k ->
   star step ge (Callstate fd args k m) t (Returnstate res k m').
-Proof (proj2 (proj2 (proj2 (proj2 bigstep_to_steps)))).
+Proof. exact (proj2 (proj2 (proj2 (proj2 bigstep_to_steps)))). Qed.
 
 Fixpoint esize (a: expr) : nat :=
   match a with
diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v
index c44acce40..7d7f37ca9 100644
--- a/cfrontend/Ctyping.v
+++ b/cfrontend/Ctyping.v
@@ -538,6 +538,7 @@ Inductive wt_program : program -> Prop :=
          wt_fundef p.(prog_comp_env) e fd) ->
       wt_program p.
 
+Create HintDb ty.
 Global Hint Constructors wt_val wt_rvalue wt_lvalue wt_stmt wt_lblstmts: ty.
 Global Hint Extern 1 (wt_int _ _ _) => exact I: ty.
 Global Hint Extern 1 (wt_int _ _ _) => reflexivity: ty.
diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v
index 04e0d5a34..ffb805197 100644
--- a/cfrontend/SimplExprproof.v
+++ b/cfrontend/SimplExprproof.v
@@ -57,25 +57,25 @@ Qed.
 
 Lemma symbols_preserved:
   forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
-Proof (Genv.find_symbol_match (proj1 TRANSL)).
+Proof. exact (Genv.find_symbol_match (proj1 TRANSL)). Qed.
 
 Lemma senv_preserved:
   Senv.equiv ge tge.
-Proof (Genv.senv_match (proj1 TRANSL)).
+Proof. exact (Genv.senv_match (proj1 TRANSL)). Qed.
 
 Lemma function_ptr_translated:
   forall b f,
   Genv.find_funct_ptr ge b = Some f ->
   exists cu tf,
   Genv.find_funct_ptr tge b = Some tf /\ tr_fundef cu f tf /\ linkorder cu prog.
-Proof (Genv.find_funct_ptr_match (proj1 TRANSL)).
+Proof. exact (Genv.find_funct_ptr_match (proj1 TRANSL)). Qed.
 
 Lemma functions_translated:
   forall v f,
   Genv.find_funct ge v = Some f ->
   exists cu tf,
   Genv.find_funct tge v = Some tf /\ tr_fundef cu f tf /\ linkorder cu prog.
-Proof (Genv.find_funct_match (proj1 TRANSL)).
+Proof. exact (Genv.find_funct_match (proj1 TRANSL)). Qed.
 
 Lemma type_of_fundef_preserved:
   forall cu f tf, tr_fundef cu f tf ->
@@ -196,12 +196,12 @@ Qed.
 Lemma tr_simple_expr_nil:
   forall le dst r sl a tmps, tr_expr ce le dst r sl a tmps ->
   dst = For_val \/ dst = For_effects -> simple r = true -> sl = nil.
-Proof (proj1 tr_simple_nil).
+Proof. exact (proj1 tr_simple_nil). Qed.
 
 Lemma tr_simple_exprlist_nil:
   forall le rl sl al tmps, tr_exprlist ce le rl sl al tmps ->
   simplelist rl = true -> sl = nil.
-Proof (proj2 tr_simple_nil).
+Proof. exact (proj2 tr_simple_nil). Qed.
 
 (** Translation of [deref_loc] and [assign_loc] operations. *)
 
diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v
index 319b7a341..dc113679f 100644
--- a/cfrontend/SimplExprspec.v
+++ b/cfrontend/SimplExprspec.v
@@ -654,6 +654,7 @@ Proof.
   elim (Plt_strict id). apply Plt_Ple_trans with (gen_next g2); auto.
 Qed.
 
+Create HintDb gensym.
 Hint Resolve gensym_within within_widen contained_widen
              contained_cons contained_app contained_disjoint
              contained_notin contained_nil
diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v
index 719b1bf9c..8fde56f5f 100644
--- a/cfrontend/SimplLocalsproof.v
+++ b/cfrontend/SimplLocalsproof.v
@@ -48,23 +48,23 @@ Qed.
 
 Lemma symbols_preserved:
   forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
-Proof (Genv.find_symbol_match (proj1 TRANSF)).
+Proof. exact (Genv.find_symbol_match (proj1 TRANSF)). Qed.
 
 Lemma senv_preserved:
   Senv.equiv ge tge.
-Proof (Genv.senv_match (proj1 TRANSF)).
+Proof. exact (Genv.senv_match (proj1 TRANSF)). Qed.
 
 Lemma functions_translated:
   forall (v: val) (f: fundef),
   Genv.find_funct ge v = Some f ->
   exists tf, Genv.find_funct tge v = Some tf /\ transf_fundef f = OK tf.
-Proof (Genv.find_funct_transf_partial (proj1 TRANSF)).
+Proof. exact (Genv.find_funct_transf_partial (proj1 TRANSF)). Qed.
 
 Lemma function_ptr_translated:
   forall (b: block) (f: fundef),
   Genv.find_funct_ptr ge b = Some f ->
   exists tf, Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf.
-Proof (Genv.find_funct_ptr_transf_partial (proj1 TRANSF)).
+Proof. exact (Genv.find_funct_ptr_transf_partial (proj1 TRANSF)). Qed.
 
 Lemma type_of_fundef_preserved:
   forall fd tfd,
@@ -580,6 +580,7 @@ Proof.
   intros; red; intros. eapply VSet.empty_1; eauto.
 Qed.
 
+Create HintDb compat.
 Hint Resolve compat_cenv_union_l compat_cenv_union_r compat_cenv_empty: compat.
 
 (** Allocation and initialization of parameters *)
diff --git a/common/Determinism.v b/common/Determinism.v
index 45fe8bf7f..03f014dea 100644
--- a/common/Determinism.v
+++ b/common/Determinism.v
@@ -504,8 +504,8 @@ Section WORLD_SEM.
 Variable L: semantics.
 Variable initial_world: world.
 
-Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope.
-Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope.
+Notation "s #1" := (fst s) (at level 1, format "s '#1'") : pair_scope.
+Notation "s #2" := (snd s) (at level 1, format "s '#2'") : pair_scope.
 Local Open Scope pair_scope.
 
 Definition world_sem : semantics := @Semantics_gen
diff --git a/common/Events.v b/common/Events.v
index 84dfb941a..38cf6139d 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -101,7 +101,7 @@ Lemma Eapp_assoc: forall t1 t2 t3, (t1 ** t2) ** t3 = t1 ** (t2 ** t3).
 Proof. intros. unfold Eapp, trace. apply app_ass. Qed.
 
 Lemma Eapp_E0_inv: forall t1 t2, t1 ** t2 = E0 -> t1 = E0 /\ t2 = E0.
-Proof (@app_eq_nil event).
+Proof. exact (@app_eq_nil event). Qed.
 
 Lemma E0_left_inf: forall T, E0 *** T = T.
 Proof. auto. Qed.
@@ -1705,6 +1705,7 @@ Qed.
 
 End EVAL_BUILTIN_ARG.
 
+Create HintDb barg.
 Global Hint Constructors eval_builtin_arg: barg.
 
 Fixpoint builtin_arg_depends_on_memory {A: Type} (ba: builtin_arg A) : bool :=
diff --git a/common/Globalenvs.v b/common/Globalenvs.v
index 9282c8e64..1a813d85c 100644
--- a/common/Globalenvs.v
+++ b/common/Globalenvs.v
@@ -40,8 +40,8 @@ Require Import Integers Floats Values Memory.
 Require Archi.
 
 Declare Scope pair_scope.
-Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope.
-Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope.
+Notation "s #1" := (fst s) (at level 1, format "s '#1'") : pair_scope.
+Notation "s #2" := (snd s) (at level 1, format "s '#2'") : pair_scope.
 Local Open Scope pair_scope.
 Local Open Scope error_monad_scope.
 
@@ -1717,7 +1717,7 @@ Qed.
 Theorem find_def_match_2:
   forall b, option_rel (match_globdef match_fundef match_varinfo ctx)
                        (find_def (globalenv p) b) (find_def (globalenv tp) b).
-Proof (mge_defs globalenvs_match).
+Proof. exact (mge_defs globalenvs_match). Qed.
 
 Theorem find_def_match:
   forall b g,
diff --git a/common/Memory.v b/common/Memory.v
index 24f7489b0..54def2786 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -3465,8 +3465,7 @@ Theorem aligned_area_inject:
 Proof.
   intros.
   assert (P: al > 0) by lia.
-  assert (Q: Z.abs al <= Z.abs sz). apply Zdivide_bounds; auto. lia.
-  rewrite Z.abs_eq in Q; try lia. rewrite Z.abs_eq in Q; try lia.
+  assert (Q: al <= sz) by (apply Z.divide_pos_le; auto; lia).
   assert (A: (min_safe_alignment sz | delta)).
   { destruct H. destruct mi_inj0. eapply mi_align0; eauto with mem. }
   assert (B: min_safe_alignment al = al).
diff --git a/common/Memtype.v b/common/Memtype.v
index 5683a38ba..78594799d 100644
--- a/common/Memtype.v
+++ b/common/Memtype.v
@@ -57,6 +57,7 @@ Inductive perm_order: permission -> permission -> Prop :=
   | perm_W_R:   perm_order Writable Readable
   | perm_any_N: forall p, perm_order p Nonempty.
 
+Create HintDb mem.
 Global Hint Constructors perm_order: mem.
 
 Lemma perm_order_trans:
diff --git a/common/Separation.v b/common/Separation.v
index 0cb7e1045..465adfa48 100644
--- a/common/Separation.v
+++ b/common/Separation.v
@@ -261,7 +261,7 @@ Qed.
 
 Lemma sep_proj2:
   forall P Q m, m |= P ** Q -> m |= Q.
-Proof sep_drop.
+Proof. exact sep_drop. Qed.
 
 Definition sep_pick1 := sep_proj1.
 
diff --git a/common/Smallstep.v b/common/Smallstep.v
index 24e1b8eb0..cefab134f 100644
--- a/common/Smallstep.v
+++ b/common/Smallstep.v
@@ -100,7 +100,7 @@ Lemma star_left:
   forall ge s1 t1 s2 t2 s3 t,
   step ge s1 t1 s2 -> star ge s2 t2 s3 -> t = t1 ** t2 ->
   star ge s1 t s3.
-Proof star_step.
+Proof. exact star_step. Qed.
 
 Lemma star_right:
   forall ge s1 t1 s2 t2 s3 t,
diff --git a/common/Unityping.v b/common/Unityping.v
index 1d46cc640..82aa25e34 100644
--- a/common/Unityping.v
+++ b/common/Unityping.v
@@ -201,6 +201,7 @@ Proof.
   apply A. rewrite PTree.gso by congruence. auto.
 Qed.
 
+Create HintDb ty.
 Global Hint Resolve set_incr: ty.
 
 Lemma set_sound:
diff --git a/configure b/configure
index 9abaf3e8e..3ed6b870e 100755
--- a/configure
+++ b/configure
@@ -98,6 +98,7 @@ Options:
   -clightgen           Also compile and install the clightgen tool
   -install-coqdev      Also install the Coq development (implied by -clightgen)
   -ignore-coq-version  Accept to use experimental or unsupported versions of Coq
+  -ignore-rocq-version  Accept to use experimental or unsupported versions of Rocq
   -ignore-ocaml-version Accept to use experimental or unsupported versions of OCaml
 '
 
@@ -136,6 +137,8 @@ while : ; do
         install_coqdev=true;;
     -ignore-coq-version|--ignore-coq-version)
         ignore_coq_version=true;;
+    -ignore-rocq-version|--ignore-rocq-version)
+        ignore_coq_version=true;;
     -ignore-ocaml-version|--ignore-ocaml-version)
         ignore_ocaml_version=true;;
     -install-coqdev|--install-coqdev|-install-coq-dev|--install-coq-dev)
@@ -531,42 +534,59 @@ fi
 # Test Availability of Required Tools
 #
 missingtools=false
+use_rocq=true
+
+echo "Testing Rocq... " | tr -d '\n'
+rocq_ver=$("${COQBIN}"rocq --print-version 2>/dev/null | tr -d '\r' | cut -d' ' -f1)
+case "$rocq_ver" in
+  9.0*|9.1*|9.2*)
+        echo "version $rocq_ver -- good!"
+        use_rocq=true;;
+  ?*)
+        echo "version $rocq_ver -- UNSUPPORTED"
+        if $ignore_coq_version; then
+            echo "Warning: this version of Rocq is unsupported, proceed at your own risks."
+        else
+            echo "Error: CompCert requires a version of Rocq between 9.0 and 9.2"
+            missingtools=true
+        fi;;
+  "")
+        echo "not found"
+        use_rocq=false;;
+esac
 
+if ! $use_rocq; then
 echo "Testing Coq... " | tr -d '\n'
 coq_ver=$("${COQBIN}"coqc --print-version 2>/dev/null | tr -d '\r' | cut -d' ' -f1)
+
 case "$coq_ver" in
-  8.15.0|8.15.1|8.15.2|8.16.0|8.16.1|8.17.0|8.17.1|8.18.0|8.19.0|8.19.1|8.19.2|8.20.0|8.20.1|9.0.0|9.1.0|9.1.1)
+  8.15.0|8.15.1|8.15.2|8.16.0|8.16.1|8.17.0|8.17.1|8.18.0|8.19.0|8.19.1|8.19.2|8.20.0|8.20.1)
         echo "version $coq_ver -- good!";;
   ?*)
         echo "version $coq_ver -- UNSUPPORTED"
         if $ignore_coq_version; then
             echo "Warning: this version of Coq is unsupported, proceed at your own risks."
         else
-            echo "Error: CompCert requires a version of Coq between 8.15 and 9.1"
+            echo "Error: CompCert requires a version of Coq between 8.15 and 8.20.1"
             missingtools=true
         fi;;
   "")
         echo "NOT FOUND"
-        rocq_ver=$("${COQBIN}"rocq --print-version 2>/dev/null | tr -d '\r' | cut -d' ' -f1)
-        case "$rocq_ver" in
-            "") echo "Error: make sure Coq is installed.";;
-             *) echo "Rocq prover version $rocq_ver found."
-                echo "Please install the Coq wrapper for this version of Rocq.";;
-        esac
         missingtools=true;;
 esac
+fi
 
 echo "Testing OCaml... " | tr -d '\n'
 ocaml_ver=$(ocamlc -version 2>/dev/null | tr -d '\r')
 case "$ocaml_ver" in
-  4.0[5-9].*|4.1?.*)
+  4.0[5-9].*|4.1?.*|5.*)
         echo "version $ocaml_ver -- good!";;
   ?.*)
         echo "version $ocaml_ver -- UNSUPPORTED"
         if $ignore_ocaml_version; then
             echo "Warning: this version of OCaml is unsupported, proceed at your own risks."
         else
-            echo "Error: make sure OCaml version 4.05 to 4.14 is installed."
+            echo "Error: make sure OCaml version 4.05 or more recent is installed."
             missingtools=true
         fi;;
   *)
@@ -698,6 +718,7 @@ OCAML_NATIVE_COMP=$ocaml_native_comp
 OCAML_OPT_COMP=$ocaml_opt_comp
 MENHIR_DIR=$menhir_dir
 COMPFLAGS=-bin-annot
+USE_ROCQ=$use_rocq
 EOF
 
 if test "$target" != "manual"; then
diff --git a/lib/Axioms.v b/lib/Axioms.v
index f6baba3b3..2e1aced47 100644
--- a/lib/Axioms.v
+++ b/lib/Axioms.v
@@ -26,21 +26,21 @@ From Coq Require ClassicalFacts FunctionalExtensionality.
 Lemma functional_extensionality_dep:
   forall {A: Type} {B : A -> Type} (f g : forall x : A, B x),
   (forall x, f x = g x) -> f = g.
-Proof @FunctionalExtensionality.functional_extensionality_dep.
+Proof. exact @FunctionalExtensionality.functional_extensionality_dep. Qed.
 
 (** and, as a corollary, functional extensionality for non-dependent functions:
 *)
 
 Lemma functional_extensionality:
   forall {A B: Type} (f g : A -> B), (forall x, f x = g x) -> f = g.
-Proof @FunctionalExtensionality.functional_extensionality.
+Proof. exact @FunctionalExtensionality.functional_extensionality. Qed.
 
 (** For compatibility with earlier developments, [extensionality]
   is an alias for [functional_extensionality]. *)
 
 Lemma extensionality:
   forall {A B: Type} (f g : A -> B),  (forall x, f x = g x) -> f = g.
-Proof @functional_extensionality.
+Proof. exact @functional_extensionality. Qed.
 
 (** * Proof irrelevance *)
 
diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index b2eb0fd33..449c8a31f 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -116,7 +116,7 @@ Global Hint Resolve Plt_ne: coqlib.
 
 Lemma Plt_trans:
   forall (x y z: positive), Plt x y -> Plt y z -> Plt x z.
-Proof (Pos.lt_trans).
+Proof. exact (Pos.lt_trans). Qed.
 
 Lemma Plt_succ:
   forall (x: positive), Plt x (Pos.succ x).
@@ -151,13 +151,13 @@ Global Opaque plt.
 Definition Ple: positive -> positive -> Prop := Pos.le.
 
 Lemma Ple_refl: forall (p: positive), Ple p p.
-Proof (Pos.le_refl).
+Proof. exact (Pos.le_refl). Qed.
 
 Lemma Ple_trans: forall (p q r: positive), Ple p q -> Ple q r -> Ple p r.
-Proof (Pos.le_trans).
+Proof. exact (Pos.le_trans). Qed.
 
 Lemma Plt_Ple: forall (p q: positive), Plt p q -> Ple p q.
-Proof (Pos.lt_le_incl).
+Proof. exact (Pos.lt_le_incl). Qed.
 
 Lemma Ple_succ: forall (p: positive), Ple p (Pos.succ p).
 Proof.
@@ -166,10 +166,10 @@ Qed.
 
 Lemma Plt_Ple_trans:
   forall (p q r: positive), Plt p q -> Ple q r -> Plt p r.
-Proof (Pos.lt_le_trans).
+Proof. exact (Pos.lt_le_trans). Qed.
 
 Lemma Plt_strict: forall p, ~ Plt p p.
-Proof (Pos.lt_irrefl).
+Proof. exact (Pos.lt_irrefl). Qed.
 
 Global Hint Resolve Ple_refl Plt_Ple Ple_succ Plt_strict: coqlib.
 
diff --git a/lib/Integers.v b/lib/Integers.v
index 38b65c647..552ffe577 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -20,6 +20,9 @@ From Coq Require Import Eqdep_dec Zquot Zwf.
 Require Import Coqlib Zbits.
 Require Archi.
 
+Create HintDb ints.
+Create HintDb ptrofs.
+
 (** Backwards compatibility for Hint Rewrite locality attributes. *)
 Set Warnings "-unsupported-attributes".
 
@@ -116,7 +119,7 @@ Definition Z_mod_modulus (x: Z) : Z :=
 
 Lemma Z_mod_modulus_range:
   forall x, 0 <= Z_mod_modulus x < modulus.
-Proof (Z_mod_two_p_range wordsize).
+Proof. exact (Z_mod_two_p_range wordsize). Qed.
 
 Lemma Z_mod_modulus_range':
   forall x, -1 < Z_mod_modulus x < modulus.
@@ -126,7 +129,7 @@ Qed.
 
 Lemma Z_mod_modulus_eq:
   forall x, Z_mod_modulus x = x mod modulus.
-Proof (Z_mod_two_p_eq wordsize).
+Proof. exact (Z_mod_two_p_eq wordsize). Qed.
 
 (** The [unsigned] and [signed] functions return the Coq integer corresponding
   to the given machine integer, interpreted as unsigned or signed
@@ -403,59 +406,59 @@ Qed.
 Definition eqm := eqmod modulus.
 
 Lemma eqm_refl: forall x, eqm x x.
-Proof (eqmod_refl modulus).
+Proof. exact (eqmod_refl modulus). Qed.
 Global Hint Resolve eqm_refl: ints.
 
 Lemma eqm_refl2:
   forall x y, x = y -> eqm x y.
-Proof (eqmod_refl2 modulus).
+Proof. exact (eqmod_refl2 modulus). Qed.
 Global Hint Resolve eqm_refl2: ints.
 
 Lemma eqm_sym: forall x y, eqm x y -> eqm y x.
-Proof (eqmod_sym modulus).
+Proof. exact (eqmod_sym modulus). Qed.
 Global Hint Resolve eqm_sym: ints.
 
 Lemma eqm_trans: forall x y z, eqm x y -> eqm y z -> eqm x z.
-Proof (eqmod_trans modulus).
+Proof. exact (eqmod_trans modulus). Qed.
 Global Hint Resolve eqm_trans: ints.
 
 Lemma eqm_small_eq:
   forall x y, eqm x y -> 0 <= x < modulus -> 0 <= y < modulus -> x = y.
-Proof (eqmod_small_eq modulus).
+Proof. exact (eqmod_small_eq modulus). Qed.
 Global Hint Resolve eqm_small_eq: ints.
 
 Lemma eqm_add:
   forall a b c d, eqm a b -> eqm c d -> eqm (a + c) (b + d).
-Proof (eqmod_add modulus).
+Proof. exact (eqmod_add modulus). Qed.
 Global Hint Resolve eqm_add: ints.
 
 Lemma eqm_neg:
   forall x y, eqm x y -> eqm (-x) (-y).
-Proof (eqmod_neg modulus).
+Proof. exact (eqmod_neg modulus). Qed.
 Global Hint Resolve eqm_neg: ints.
 
 Lemma eqm_sub:
   forall a b c d, eqm a b -> eqm c d -> eqm (a - c) (b - d).
-Proof (eqmod_sub modulus).
+Proof. exact (eqmod_sub modulus). Qed.
 Global Hint Resolve eqm_sub: ints.
 
 Lemma eqm_mult:
   forall a b c d, eqm a c -> eqm b d -> eqm (a * b) (c * d).
-Proof (eqmod_mult modulus).
+Proof. exact (eqmod_mult modulus). Qed.
 Global Hint Resolve eqm_mult: ints.
 
 Lemma eqm_same_bits:
   forall x y,
   (forall i, 0 <= i < zwordsize -> Z.testbit x i = Z.testbit y i) ->
   eqm x y.
-Proof (eqmod_same_bits wordsize).
+Proof. exact (eqmod_same_bits wordsize). Qed.
 
 Lemma same_bits_eqm:
   forall x y i,
   eqm x y ->
   0 <= i < zwordsize ->
   Z.testbit x i = Z.testbit y i.
-Proof (same_bits_eqmod wordsize).
+Proof. exact (same_bits_eqmod wordsize). Qed.
 
 (** ** Properties of the coercions between [Z] and [int] *)
 
diff --git a/lib/Intv.v b/lib/Intv.v
index 69b55eae8..e6605dbc6 100644
--- a/lib/Intv.v
+++ b/lib/Intv.v
@@ -263,6 +263,8 @@ Qed.
 
 (** Hints *)
 
+Create HintDb intv.
+
 Global Hint Resolve
   notin_range range_notin
   is_notempty empty_notin in_notempty
diff --git a/lib/Lattice.v b/lib/Lattice.v
index 6431ad991..6db23edd3 100644
--- a/lib/Lattice.v
+++ b/lib/Lattice.v
@@ -188,6 +188,7 @@ Proof.
   auto.
 Qed.
 
+Create HintDb combine.
 Local Hint Resolve opt_beq_correct opt_eq_refl opt_eq_sym : combine.
 
 (** A [combine] operation over the type [PTree.t L.t] that attempts
@@ -746,7 +747,7 @@ Definition eq_trans: forall x y z, eq x y -> eq y z -> eq x z := (@eq_trans t).
 Definition beq : t -> t -> bool := eqb.
 
 Lemma beq_correct: forall x y, beq x y = true -> eq x y.
-Proof eqb_prop.
+Proof. exact eqb_prop. Qed.
 
 Definition ge (x y: t) : Prop := x = y \/ x = true.
 
diff --git a/lib/Maps.v b/lib/Maps.v
index b85b653b5..55fdc9ce3 100644
--- a/lib/Maps.v
+++ b/lib/Maps.v
@@ -763,7 +763,7 @@ Module PTree <: TREE.
 
   Lemma prev_involutive i :
     prev (prev i) = i.
-  Proof (prev_append_prev i xH).
+  Proof. exact (prev_append_prev i xH). Qed.
 
   Lemma prev_append_inj i j j' :
     prev_append i j = prev_append i j' -> j = j'.
diff --git a/lib/Ordered.v b/lib/Ordered.v
index c22c47097..dea43c7da 100644
--- a/lib/Ordered.v
+++ b/lib/Ordered.v
@@ -31,15 +31,15 @@ Definition eq (x y: t) := x = y.
 Definition lt := Plt.
 
 Lemma eq_refl : forall x : t, eq x x.
-Proof (@eq_refl t).
+Proof. exact (@eq_refl t). Qed.
 Lemma eq_sym : forall x y : t, eq x y -> eq y x.
-Proof (@eq_sym t).
+Proof. exact (@eq_sym t). Qed.
 Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
-Proof (@eq_trans t).
+Proof. exact (@eq_trans t). Qed.
 Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
-Proof Plt_trans.
+Proof. exact Plt_trans. Qed.
 Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
-Proof Plt_ne.
+Proof. exact Plt_ne. Qed.
 Lemma compare : forall x y : t, Compare lt eq x y.
 Proof.
   intros. destruct (Pos.compare x y) as [] eqn:E.
@@ -61,13 +61,13 @@ Definition eq (x y: t) := x = y.
 Definition lt := Z.lt.
 
 Lemma eq_refl : forall x : t, eq x x.
-Proof (@eq_refl t).
+Proof. exact (@eq_refl t). Qed.
 Lemma eq_sym : forall x y : t, eq x y -> eq y x.
-Proof (@eq_sym t).
+Proof. exact (@eq_sym t). Qed.
 Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
-Proof (@eq_trans t).
+Proof. exact (@eq_trans t). Qed.
 Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
-Proof Z.lt_trans.
+Proof. exact Z.lt_trans. Qed.
 Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
 Proof. unfold lt, eq, t; intros. lia. Qed.
 Lemma compare : forall x y : t, Compare lt eq x y.
@@ -91,11 +91,11 @@ Definition eq (x y: t) := x = y.
 Definition lt (x y: t) := Int.unsigned x < Int.unsigned y.
 
 Lemma eq_refl : forall x : t, eq x x.
-Proof (@eq_refl t).
+Proof. exact (@eq_refl t). Qed.
 Lemma eq_sym : forall x y : t, eq x y -> eq y x.
-Proof (@eq_sym t).
+Proof. exact (@eq_sym t). Qed.
 Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
-Proof (@eq_trans t).
+Proof. exact (@eq_trans t). Qed.
 Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
 Proof.
   unfold lt; intros. lia.
@@ -129,11 +129,11 @@ Definition eq (x y: t) := x = y.
 Definition lt (x y: t) := Plt (A.index x) (A.index y).
 
 Lemma eq_refl : forall x : t, eq x x.
-Proof (@eq_refl t).
+Proof. exact (@eq_refl t). Qed.
 Lemma eq_sym : forall x y : t, eq x y -> eq y x.
-Proof (@eq_sym t).
+Proof. exact (@eq_sym t). Qed.
 Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
-Proof (@eq_trans t).
+Proof. exact (@eq_trans t). Qed.
 
 Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
 Proof.
diff --git a/lib/Parmov.v b/lib/Parmov.v
index 6db299f62..0ec9c8cfd 100644
--- a/lib/Parmov.v
+++ b/lib/Parmov.v
@@ -99,7 +99,7 @@ Definition env := reg -> val.
 Lemma env_ext:
   forall (e1 e2: env),
   (forall r, e1 r = e2 r) -> e1 = e2.
-Proof (@extensionality reg val).
+Proof. exact (@extensionality reg val). Qed.
 
 (** The main operation over environments is update: it assigns
   a value [v] to a register [r] and preserves the values of other
diff --git a/lib/Zbits.v b/lib/Zbits.v
index 6470912c7..cce9624ad 100644
--- a/lib/Zbits.v
+++ b/lib/Zbits.v
@@ -204,7 +204,7 @@ Definition Zshiftin (b: bool) (x: Z) : Z :=
   if b then Z.succ_double x else Z.double x.
 
 Remark Ztestbit_0: forall n, Z.testbit 0 n = false.
-Proof Z.testbit_0_l.
+Proof. exact Z.testbit_0_l. Qed.
 
 Remark Ztestbit_1: forall n, Z.testbit 1 n = zeq n 0.
 Proof.
@@ -370,7 +370,7 @@ Lemma equal_same_bits:
   forall x y,
   (forall i, 0 <= i -> Z.testbit x i = Z.testbit y i) ->
   x = y.
-Proof Z.bits_inj'.
+Proof. exact Z.bits_inj'. Qed.
 
 Lemma Z_one_complement:
   forall i, 0 <= i ->
diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index 9ab01e045..3486d54e7 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -39,18 +39,18 @@ Let tge := Genv.globalenv tprog.
 
 Lemma symbols_preserved:
   forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
-Proof (Genv.find_symbol_match TRANSF).
+Proof. exact (Genv.find_symbol_match TRANSF). Qed.
 
 Lemma senv_preserved:
   Senv.equiv ge tge.
-Proof (Genv.senv_match TRANSF).
+Proof. exact (Genv.senv_match TRANSF). Qed.
 
 Lemma functions_translated:
   forall b f,
   Genv.find_funct_ptr ge b = Some f ->
   exists tf,
   Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf.
-Proof (Genv.find_funct_ptr_transf_partial TRANSF).
+Proof. exact (Genv.find_funct_ptr_transf_partial TRANSF). Qed.
 
 Lemma functions_transl:
   forall fb f tf,
diff --git a/riscV/Asmgenproof.v b/riscV/Asmgenproof.v
index ed841616b..553f1179d 100644
--- a/riscV/Asmgenproof.v
+++ b/riscV/Asmgenproof.v
@@ -37,18 +37,18 @@ Let tge := Genv.globalenv tprog.
 
 Lemma symbols_preserved:
   forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
-Proof (Genv.find_symbol_match TRANSF).
+Proof. exact (Genv.find_symbol_match TRANSF). Qed.
 
 Lemma senv_preserved:
   Senv.equiv ge tge.
-Proof (Genv.senv_match TRANSF).
+Proof. exact (Genv.senv_match TRANSF). Qed.
 
 Lemma functions_translated:
   forall b f,
   Genv.find_funct_ptr ge b = Some f ->
   exists tf,
   Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf.
-Proof (Genv.find_funct_ptr_transf_partial TRANSF).
+Proof. exact (Genv.find_funct_ptr_transf_partial TRANSF). Qed.
 
 Lemma functions_transl:
   forall fb f tf,
@@ -281,15 +281,7 @@ Opaque Int.eq.
 - destruct (SelectOp.symbol_is_relocatable id && negb (Ptrofs.eq ofs Ptrofs.zero)).
 + eapply tail_nolabel_trans; [|apply addptrofs_label]. TailNoLabel.
 + TailNoLabel. 
-- apply opimm32_label; intros; exact I.
-- apply opimm32_label; intros; exact I.
-- apply opimm32_label; intros; exact I.
-- apply opimm32_label; intros; exact I.
 - destruct (Int.eq n Int.zero); TailNoLabel.
-- apply opimm64_label; intros; exact I.
-- apply opimm64_label; intros; exact I.
-- apply opimm64_label; intros; exact I.
-- apply opimm64_label; intros; exact I.
 - destruct (Int.eq n Int.zero); TailNoLabel.
 - eapply transl_cond_op_label; eauto.
 - eapply tail_nolabel_trans; eauto using transl_cond_op_label; TailNoLabel.
diff --git a/x86/Asmgenproof.v b/x86/Asmgenproof.v
index 67c42b2ba..61beb74bf 100644
--- a/x86/Asmgenproof.v
+++ b/x86/Asmgenproof.v
@@ -37,18 +37,18 @@ Let tge := Genv.globalenv tprog.
 
 Lemma symbols_preserved:
   forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
-Proof (Genv.find_symbol_match TRANSF).
+Proof. exact (Genv.find_symbol_match TRANSF). Qed.
 
 Lemma senv_preserved:
   Senv.equiv ge tge.
-Proof (Genv.senv_match TRANSF).
+Proof. exact (Genv.senv_match TRANSF). Qed.
 
 Lemma functions_translated:
   forall b f,
   Genv.find_funct_ptr ge b = Some f ->
   exists tf,
   Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf.
-Proof (Genv.find_funct_ptr_transf_partial TRANSF).
+Proof. exact (Genv.find_funct_ptr_transf_partial TRANSF). Qed.
 
 Lemma functions_transl:
   forall fb f tf,