From 04e9be59051ca60bf61d5142ac14386920876926 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Fri, 18 Sep 2015 08:00:14 +0200
Subject: Do not compress match constructs when the inner match contains no
 branch. (Fix bug #4348)

---
 pretyping/detyping.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 28fb8cbe36..8bd57290b0 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -276,6 +276,7 @@ and align_tree nal isgoal (e,c as rhs) = match nal with
     match kind_of_term c with
     | Case (ci,p,c,cl) when
         eq_constr c (mkRel (List.index Name.equal na (fst (snd e))))
+        && not (Int.equal (Array.length cl) 0)
 	&& (* don't contract if p dependent *)
 	computable p (List.length ci.ci_pp_info.ind_tags) (* FIXME: can do better *) ->
 	let clauses = build_tree na isgoal e ci cl in
-- 
cgit v1.2.3


From bfd0ee9503cf04b51b2dd40d4ad2a904b07ac323 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Sun, 20 Sep 2015 00:06:33 +0200
Subject: Fix #3948 Anomaly: unknown constant in Print Assumptions

Substitution on bound modules was incorrectly extended without sequential
composition.
---
 kernel/mod_subst.ml     |  2 +-
 kernel/mod_subst.mli    |  5 +++--
 toplevel/assumptions.ml | 12 ++++++------
 3 files changed, 10 insertions(+), 9 deletions(-)

diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index f7ae30e7af..ba14f65d9e 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -122,7 +122,7 @@ let add_kn_delta_resolver kn kn' =
 
 let add_mp_delta_resolver mp1 mp2 = Deltamap.add_mp mp1 mp2
 
-(** Extending a [substitution] *)
+(** Extending a [substitution] without sequential composition *)
 
 let add_mbid mbid mp resolve s = Umap.add_mbi mbid (mp,resolve) s
 let add_mp mp1 mp2 resolve s = Umap.add_mp mp1 (mp2,resolve) s
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli
index fc2b0441ca..cd9fa79216 100644
--- a/kernel/mod_subst.mli
+++ b/kernel/mod_subst.mli
@@ -68,8 +68,9 @@ val empty_subst : substitution
 
 val is_empty_subst : substitution -> bool
 
-(** add_* add [arg2/arg1]\{arg3\} to the substitution with no
-   sequential composition  *)
+(** add_* add [arg2/arg1]\{arg3\} to the substitution with no sequential
+   composition. Most often this is not what you want. For sequential
+   composition, try [join (map_mbid mp delta) subs] **)
 val add_mbid :
   MBId.t -> module_path -> delta_resolver  -> substitution -> substitution
 val add_mp :
diff --git a/toplevel/assumptions.ml b/toplevel/assumptions.ml
index 4d8ba0f789..a6bd968efc 100644
--- a/toplevel/assumptions.ml
+++ b/toplevel/assumptions.ml
@@ -55,7 +55,7 @@ let rec fields_of_functor f subs mp0 args = function
     match args with
     | [] -> assert false (* we should only encounter applied functors *)
     | mpa :: args ->
-      let subs = add_mbid mbid mpa empty_delta_resolver (*TODO*) subs in
+      let subs = join (map_mbid mbid mpa empty_delta_resolver (*TODO*)) subs in
       fields_of_functor f subs mp0 args e
 
 let rec lookup_module_in_impl mp =
@@ -64,11 +64,11 @@ let rec lookup_module_in_impl mp =
     (* The module we search might not be exported by its englobing module(s).
        We access the upper layer, and then do a manual search *)
     match mp with
-      | MPfile _ | MPbound _ ->
-	raise Not_found (* should have been found by [lookup_module] *)
-      | MPdot (mp',lab') ->
-	let fields = memoize_fields_of_mp mp' in
-	search_mod_label lab' fields
+    | MPfile _ -> raise Not_found (* can happen if mp is an open module *)
+    | MPbound _ -> assert false
+    | MPdot (mp',lab') ->
+       let fields = memoize_fields_of_mp mp' in
+       search_mod_label lab' fields
 
 and memoize_fields_of_mp mp =
   try MPmap.find mp !modcache
-- 
cgit v1.2.3


From b712864e9cf499f1298c1aca1ad8a8b17e145079 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 18 Sep 2015 12:12:05 +0200
Subject: Revert "On MacOS X, ensuring that files found in the file system have
 the" and "Continuing incomplete 4b5af0d6e9ec1 (on MacOS X, ensuring that
 files" and "Continuing 4b5af0d6e9 and 69941d4e19 about filename case check on
 MacOS X."

This reverts commits 4b5af0d6e9ec1343a2c3ff9f856a019fa93c3606
and 69941d4e195650bf59285b897c14d6287defea0f
and e7043eec55085f4101bfb126d8829de6f6086c5a.

Trying to emulate a case sensitive file system on top of a case aware one is
too costly: 3x slowdown when compiling the stdlib or CompCert.
---
 lib/envars.ml  | 19 +++----------------
 lib/system.ml  | 16 ++--------------
 lib/system.mli |  2 --
 3 files changed, 5 insertions(+), 32 deletions(-)

diff --git a/lib/envars.ml b/lib/envars.ml
index ac0b6f722e..b0eed8386b 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -39,25 +39,12 @@ let path_to_list p =
 let user_path () =
   path_to_list (Sys.getenv "PATH") (* may raise Not_found *)
 
-  (* Duplicated from system.ml to minimize dependencies *)
-let file_exists_respecting_case f =
-  if Coq_config.arch = "Darwin" then
-    (* ensure that the file exists with expected case on the
-       case-insensitive but case-preserving default MacOS file system *)
-    let rec aux f =
-      let bf = Filename.basename f in
-      let df = Filename.dirname f in
-      String.equal df "." || String.equal df "/" ||
-      aux df && Array.exists (String.equal bf) (Sys.readdir df)
-    in aux f
-  else Sys.file_exists f
-
 let rec which l f =
   match l with
     | [] ->
       raise Not_found
     | p :: tl ->
-      if file_exists_respecting_case (p / f) then
+      if Sys.file_exists (p / f) then
 	p
       else
 	which tl f
@@ -115,7 +102,7 @@ let _ =
     If the check fails, then [oth ()] is evaluated. *)
 let check_file_else ~dir ~file oth =
   let path = if Coq_config.local then coqroot else coqroot / dir in
-  if file_exists_respecting_case (path / file) then path else oth ()
+  if Sys.file_exists (path / file) then path else oth ()
 
 let guess_coqlib fail =
   let prelude = "theories/Init/Prelude.vo" in
@@ -147,7 +134,7 @@ let coqpath =
   let coqpath = getenv_else "COQPATH" (fun () -> "") in
   let make_search_path path =
     let paths = path_to_list path in
-    let valid_paths = List.filter file_exists_respecting_case paths in
+    let valid_paths = List.filter Sys.file_exists paths in
     List.rev valid_paths
   in
   make_search_path coqpath
diff --git a/lib/system.ml b/lib/system.ml
index 27e21204cc..d1cdd8efc9 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -53,18 +53,6 @@ let all_subdirs ~unix_path:root =
   if exists_dir root then traverse root [];
   List.rev !l
 
-let file_exists_respecting_case f =
-  if Coq_config.arch = "Darwin" then
-    (* ensure that the file exists with expected case on the
-       case-insensitive but case-preserving default MacOS file system *)
-    let rec aux f =
-      let bf = Filename.basename f in
-      let df = Filename.dirname f in
-      (String.equal df "." || String.equal df "/" || aux df)
-      && Array.exists (String.equal bf) (Sys.readdir df)
-    in aux f
-  else Sys.file_exists f
-
 let rec search paths test =
   match paths with
   | [] -> []
@@ -89,7 +77,7 @@ let where_in_path ?(warn=true) path filename =
   in
   check_and_warn (search path (fun lpe ->
     let f = Filename.concat lpe filename in
-    if file_exists_respecting_case f then [lpe,f] else []))
+    if Sys.file_exists f then [lpe,f] else []))
 
 let where_in_path_rex path rex =
   search path (fun lpe ->
@@ -105,7 +93,7 @@ let where_in_path_rex path rex =
 
 let find_file_in_path ?(warn=true) paths filename =
   if not (Filename.is_implicit filename) then
-    if file_exists_respecting_case filename then
+    if Sys.file_exists filename then
       let root = Filename.dirname filename in
       root, filename
     else
diff --git a/lib/system.mli b/lib/system.mli
index 051e92f166..a3d66d577a 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -29,8 +29,6 @@ val exists_dir : string -> bool
 val find_file_in_path :
   ?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string
 
-val file_exists_respecting_case : string -> bool
-
 (** {6 I/O functions } *)
 (** Generic input and output functions, parameterized by a magic number
   and a suffix. The intern functions raise the exception [Bad_magic_number]
-- 
cgit v1.2.3


From bcba542aac3e17bab78f74e0fd3600e12cc0e492 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Sun, 20 Sep 2015 00:23:59 +0200
Subject: Test file for #3948 - Anomaly: unknown constant in Print Assumptions.

---
 test-suite/bugs/closed/3948.v | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)
 create mode 100644 test-suite/bugs/closed/3948.v

diff --git a/test-suite/bugs/closed/3948.v b/test-suite/bugs/closed/3948.v
new file mode 100644
index 0000000000..56b1e3ffb4
--- /dev/null
+++ b/test-suite/bugs/closed/3948.v
@@ -0,0 +1,24 @@
+Module Type S.
+Parameter t : Type.
+End S.
+
+Module Bar(X : S).
+Definition elt := X.t.
+Axiom fold : elt.
+End Bar.
+
+Module Make (Z: S) := Bar(Z).
+
+Declare Module Y : S.
+
+Module Type Interface.
+Parameter constant : unit.
+End Interface.
+
+Module DepMap : Interface.
+Module Dom := Make(Y).
+Definition constant : unit :=
+  let _ := @Dom.fold in tt.
+End DepMap.
+
+Print Assumptions DepMap.constant.
-- 
cgit v1.2.3


From 7f0346ea0cc5d76ff7c5aa6f95cfd43769ae21aa Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Sun, 20 Sep 2015 00:56:02 +0200
Subject: Remove unused type_in_type field in safe_env.

Was left over after Hugo's 9c732a5c878b.
---
 kernel/safe_typing.ml | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 907ad2a1d4..55e767321b 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -81,8 +81,7 @@ open Declarations
       These fields could be deduced from [revstruct], but they allow faster
       name freshness checks.
  - [univ] and [future_cst] : current and future universe constraints
- - [engagement] : are we Set-impredicative?
- - [type_in_type] : does the universe hierarchy collapse?
+ - [engagement] : are we Set-impredicative? does the universe hierarchy collapse?
  - [required] : names and digests of Require'd libraries since big-bang.
       This field will only grow
  - [loads] : list of libraries Require'd inside the current module.
@@ -122,7 +121,6 @@ type safe_environment =
     univ : Univ.constraints;
     future_cst : Univ.constraints Future.computation list;
     engagement : engagement option;
-    type_in_type : bool;
     required : vodigest DPMap.t;
     loads : (module_path * module_body) list;
     local_retroknowledge : Retroknowledge.action list;
@@ -152,7 +150,6 @@ let empty_environment =
     future_cst = [];
     univ = Univ.Constraint.empty;
     engagement = None;
-    type_in_type = false;
     required = DPMap.empty;
     loads = [];
     local_retroknowledge = [];
-- 
cgit v1.2.3


From 40479227cba680496bf358e196e57a9a64f9c65b Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Sun, 20 Sep 2015 00:58:25 +0200
Subject: Nametab: print debug notice only in debug mode.

---
 library/nametab.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/library/nametab.ml b/library/nametab.ml
index 6af1e686b0..5b6d7cd982 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -524,7 +524,8 @@ let shortest_qualid_of_tactic kn =
 
 let pr_global_env env ref =
   try str (string_of_qualid (shortest_qualid_of_global env ref))
-  with Not_found as e -> prerr_endline "pr_global_env not found"; raise e
+  with Not_found as e ->
+    if !Flags.debug then Pp.msg_debug (Pp.str "pr_global_env not found"); raise e
 
 let global_inductive r =
   match global r with
-- 
cgit v1.2.3


From 0c766b2e3b54d96713a79e40661653c5486822a8 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Sun, 20 Sep 2015 01:23:26 +0200
Subject: Print Assumptions shows engagement.

Seems to be morally required since we have the -type-in-type flag.
---
 printing/printer.ml | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

diff --git a/printing/printer.ml b/printing/printer.ml
index 33b95c2f56..18e4902255 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -742,7 +742,8 @@ module ContextObjectSet = Set.Make (OrderedContextObject)
 module ContextObjectMap = Map.Make (OrderedContextObject)
 
 let pr_assumptionset env s =
-  if ContextObjectMap.is_empty s then
+  if ContextObjectMap.is_empty s &&
+       engagement env = (PredicativeSet, StratifiedType) then
     str "Closed under the global context"
   else
     let safe_pr_constant env kn =
@@ -788,6 +789,16 @@ let pr_assumptionset env s =
     let (vars, axioms, opaque, trans) = 
       ContextObjectMap.fold fold s ([], [], [], [])
     in
+    let theory =
+      if is_impredicative_set env then
+	[str "Set is impredicative"]
+      else []
+    in
+    let theory =
+      if type_in_type env then
+	str "Type hierarchy is collapsed (logic is inconsistent)" :: theory
+      else theory
+    in
     let opt_list title = function
     | [] -> None
     | l ->
@@ -801,6 +812,7 @@ let pr_assumptionset env s =
       opt_list (str "Section Variables:") vars;
       opt_list (str "Axioms:") axioms;
       opt_list (str "Opaque constants:") opaque;
+      opt_list (str "Theory:") theory;
     ] in
     prlist_with_sep fnl (fun x -> x) (Option.List.flatten assums)
 
-- 
cgit v1.2.3


From b3bd2696c31ad2cb544f3436ddb5a237fe7fa6fe Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Sun, 20 Sep 2015 15:34:19 +0200
Subject: Proof: suggest Admitted->Qed only if the proof is really complete
 (#4349)

---
 proofs/proof.ml        | 10 ++++++++--
 proofs/proof.mli       |  3 +++
 proofs/proof_global.ml |  2 +-
 3 files changed, 12 insertions(+), 3 deletions(-)

diff --git a/proofs/proof.ml b/proofs/proof.ml
index a7077d9110..c7aa5bad97 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -173,6 +173,12 @@ let is_done p =
 (* spiwack: for compatibility with <= 8.2 proof engine *)
 let has_unresolved_evar p =
   Proofview.V82.has_unresolved_evar p.proofview
+let has_shelved_goals p = not (CList.is_empty (p.shelf))
+let has_given_up_goals p = not (CList.is_empty (p.given_up))
+
+let is_complete p =
+  is_done p && not (has_unresolved_evar p) &&
+  not (has_shelved_goals p) && not (has_given_up_goals p)
 
 (* Returns the list of partial proofs to initial goals *)
 let partial_proof p = Proofview.partial_proof p.entry p.proofview
@@ -305,9 +311,9 @@ end
 let return p =
   if not (is_done p) then
     raise UnfinishedProof
-  else if not (CList.is_empty (p.shelf)) then
+  else if has_shelved_goals p then
     raise HasShelvedGoals
-  else if not (CList.is_empty (p.given_up)) then
+  else if has_given_up_goals p then
     raise HasGivenUpGoals
   else if has_unresolved_evar p then
     (* spiwack: for compatibility with <= 8.3 proof engine *)
diff --git a/proofs/proof.mli b/proofs/proof.mli
index a2e10d8133..a0ed0654db 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -75,6 +75,9 @@ val initial_euctx : proof -> Evd.evar_universe_context
     to be considered (this does not require that all evars have been solved). *)
 val is_done : proof -> bool
 
+(* Like is_done, but this time it really means done (i.e. nothing left to do) *)
+val is_complete : proof -> bool
+
 (* Returns the list of partial proofs to initial goals. *)
 val partial_proof : proof -> Term.constr list
 
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index c02b909164..6c963bf705 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -341,7 +341,7 @@ type closed_proof_output = (Term.constr * Declareops.side_effects) list * Evd.ev
 let return_proof ?(allow_partial=false) () =
  let { pid; proof; strength = (_,poly,_) } = cur_pstate () in
  if allow_partial then begin
-  if Proof.is_done proof then begin
+  if Proof.is_complete proof then begin
     msg_warning (str"The proof of " ++ str (Names.Id.to_string pid) ++
      str" is complete, no need to end it with Admitted");
   end;
-- 
cgit v1.2.3


From 0ac3a2f4de0dc02b973c9f5d59b3c0a97f888141 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 21 Sep 2015 10:35:56 +0200
Subject: Change the default modifiers for navigation. (Fix bug #4295)

On most systems (including Windows, according to the bug report), shortcuts
Ctrl+Alt+Arrows are preempted by the window manager by default. So don't
use them for navigation in Coqide by default. Note that this change only
has an impact when installing on a fresh system; it won't change anything
for existing users.
---
 ide/preferences.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/ide/preferences.ml b/ide/preferences.ml
index 1bd9f587c7..90862d0647 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -190,7 +190,7 @@ let current = {
     automatic_tactics = ["trivial"; "tauto"; "auto"; "omega";
 			 "auto with *"; "intuition" ];
 
-    modifier_for_navigation = "<Control><Alt>";
+    modifier_for_navigation = "<Control>";
     modifier_for_templates = "<Control><Shift>";
     modifier_for_tactics = "<Control><Alt>";
     modifier_for_display = "<Alt><Shift>";
-- 
cgit v1.2.3


From 7c5356ed487dcf7cf915e5471832852f7002586c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 21 Sep 2015 15:54:19 +0200
Subject: Fixing tutorial.

The V7 to V8 translator lost part of term annotations.
---
 doc/tutorial/Tutorial.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex
index 836944ab1c..e09feeb8eb 100644
--- a/doc/tutorial/Tutorial.tex
+++ b/doc/tutorial/Tutorial.tex
@@ -208,7 +208,7 @@ Definition two : nat := S one.
 
 Actually \Coq~ allows several possible syntaxes:
 \begin{coq_example}
-Definition three : nat := S two.
+Definition three := S two : nat.
 \end{coq_example}
 
 Here is a way to define the doubling function, which expects an
-- 
cgit v1.2.3


From e1146f44229b380a8f52c67e1a51df4d6c03086e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 22 Sep 2015 15:40:40 +0200
Subject: Fixing bug #4207: setoid_rewrite creates self-referring hypotheses.

We purge the environment given to the morphism searcher from all dependencies
on the considered variable. I hope it is not too costly.
---
 tactics/rewrite.ml | 24 ++++++++++++++++--------
 1 file changed, 16 insertions(+), 8 deletions(-)

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index aa057a3e86..3c4550a3cf 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1542,7 +1542,7 @@ let newfail n s =
 
 let cl_rewrite_clause_newtac ?abs ?origsigma strat clause =
   let open Proofview.Notations in
-  let treat sigma (res, is_hyp) = 
+  let treat sigma res = 
     match res with
     | None -> newfail 0 (str "Nothing to rewrite")
     | Some None -> Proofview.tclUNIT ()
@@ -1550,7 +1550,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma strat clause =
         let (undef, prf, newt) = res in
         let fold ev _ accu = if Evd.mem sigma ev then accu else ev :: accu in
         let gls = List.rev (Evd.fold_undefined fold undef []) in
-	match is_hyp, prf with
+	match clause, prf with
 	| Some id, Some p ->
             let tac = Proofview.Refine.refine ~unsafe:false (fun h -> (h, p)) <*> Proofview.Unsafe.tclNEWGOALS gls in
             Proofview.Unsafe.tclEVARS undef <*>
@@ -1582,17 +1582,25 @@ let cl_rewrite_clause_newtac ?abs ?origsigma strat clause =
     let concl = Proofview.Goal.concl gl in
     let env = Proofview.Goal.env gl in
     let sigma = Proofview.Goal.sigma gl in
-    let ty, is_hyp =
-      match clause with
-      | Some id -> Environ.named_type id env, Some id
-      | None -> concl, None
+    let ty = match clause with
+    | None -> concl
+    | Some id -> Environ.named_type id env
+    in
+    let env = match clause with
+    | None -> env
+    | Some id ->
+      (** Only consider variables not depending on [id] *)
+      let ctx = Environ.named_context env in
+      let filter decl = not (occur_var_in_decl env id decl) in
+      let nctx = List.filter filter ctx in
+      Environ.reset_with_named_context (Environ.val_of_named_context nctx) env
     in
     try
       let res =
-        cl_rewrite_clause_aux ?abs strat env [] sigma ty is_hyp
+        cl_rewrite_clause_aux ?abs strat env [] sigma ty clause
       in
       let sigma = match origsigma with None -> sigma | Some sigma -> sigma in
-      treat sigma (res, is_hyp) <*>
+      treat sigma res <*>
       (** For compatibility *)
       beta <*> opt_beta <*> Proofview.shelve_unifiable
     with
-- 
cgit v1.2.3


From 6459c0e8c240f0997873c50d4ec749effaba2f44 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 31 Jul 2015 18:33:06 +0200
Subject: Removing the generalization of the body of inductive schemes from
 Auto_ind_decl over the internal lemmas. The schemes are built in the main
 process and the internal lemmas are actually already also in the environment.

---
 proofs/pfedit.ml          | 4 ++--
 proofs/pfedit.mli         | 2 +-
 toplevel/auto_ind_decl.ml | 6 +++---
 3 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index c77ab06b94..ceb4facc1e 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -145,12 +145,12 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo
     delete_current_proof ();
     iraise reraise
 
-let build_by_tactic env ctx ?(poly=false) typ tac =
+let build_by_tactic ?(side_eff=true) env ctx ?(poly=false) typ tac =
   let id = Id.of_string ("temporary_proof"^string_of_int (next())) in
   let sign = val_of_named_context (named_context env) in
   let gk = Global, poly, Proof Theorem in
   let ce, status, univs = build_constant_by_tactic id ctx sign ~goal_kind:gk typ tac in
-  let ce = Term_typing.handle_entry_side_effects env ce in
+  let ce = if side_eff then Term_typing.handle_entry_side_effects env ce else { ce with const_entry_body = Future.chain ~pure:true ce.const_entry_body (fun (pt, _) -> pt, Declareops.no_seff) } in
   let (cb, ctx), se = Future.force ce.const_entry_body in
   assert(Declareops.side_effects_is_empty se);
   assert(Univ.ContextSet.is_empty ctx);
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 5e0fb4dd36..4aa3c3bfd2 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -153,7 +153,7 @@ val build_constant_by_tactic :
   types -> unit Proofview.tactic -> 
   Entries.definition_entry * bool * Evd.evar_universe_context
 
-val build_by_tactic : env -> Evd.evar_universe_context -> ?poly:polymorphic -> 
+val build_by_tactic : ?side_eff:bool -> env -> Evd.evar_universe_context -> ?poly:polymorphic ->
   types -> unit Proofview.tactic -> 
   constr * bool * Evd.evar_universe_context
 
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index d1452fca21..16683d243e 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -637,7 +637,7 @@ let make_bl_scheme mind =
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
   let bl_goal, eff = compute_bl_goal ind lnamesparrec nparrec in
   let ctx = Evd.empty_evar_universe_context (*FIXME univs *) in
-  let (ans, _, ctx) = Pfedit.build_by_tactic (Global.env()) ctx bl_goal
+  let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff:false (Global.env()) ctx bl_goal
     (compute_bl_tact (!bl_scheme_kind_aux()) (ind, Univ.Instance.empty) lnamesparrec nparrec)
   in
   ([|ans|], ctx), eff
@@ -759,7 +759,7 @@ let make_lb_scheme mind =
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
   let lb_goal, eff = compute_lb_goal ind lnamesparrec nparrec in
   let ctx = Evd.empty_evar_universe_context in
-  let (ans, _, ctx) = Pfedit.build_by_tactic (Global.env()) ctx lb_goal
+  let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff:false (Global.env()) ctx lb_goal
     (compute_lb_tact (!lb_scheme_kind_aux()) ind lnamesparrec nparrec)
   in
   ([|ans|], ctx (* FIXME *)), eff
@@ -930,7 +930,7 @@ let make_eq_decidability mind =
   let ctx = Evd.empty_evar_universe_context (* FIXME *)in
   let lnonparrec,lnamesparrec =
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
-  let (ans, _, ctx) = Pfedit.build_by_tactic (Global.env()) ctx
+  let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff:false (Global.env()) ctx
     (compute_dec_goal (ind,u) lnamesparrec nparrec)
     (compute_dec_tact ind lnamesparrec nparrec)
   in
-- 
cgit v1.2.3


From 13716dc6561a3379ba130f07ce7ecd1df379475c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 31 Jul 2015 18:45:41 +0200
Subject: Give a way to control if the decidable-equality schemes are built
 like in 8.4 with the schemes of the subcomponent of an inductive added to the
 environment or discharged as let-ins over the main scheme.

As of today, decidable-equality schemes are built when calling
vernacular command (Inductive with option Set Dedicable Equality
Schemes, or Scheme Equality), so there is no need to discharge the
sub-schemes as let-ins. But if ever the schemes are built from within
an opaque proof and one would not like the schemes and a fortiori the
subschemes to appear in the env, the new addition of a parameter
internal_flag to "find_scheme" allows this possibility (then to be set
to KernelSilent).
---
 tactics/elimschemes.ml    | 20 ++++++++++----------
 tactics/eqschemes.ml      | 18 +++++++++---------
 toplevel/auto_ind_decl.ml | 42 +++++++++++++++++++++++++-----------------
 toplevel/ind_tables.ml    | 32 +++++++++++++++-----------------
 toplevel/ind_tables.mli   | 15 ++++++---------
 5 files changed, 65 insertions(+), 62 deletions(-)

diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index e1c9c2de59..e6a8cbe3ad 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -21,7 +21,7 @@ open Ind_tables
 
 (* Induction/recursion schemes *)
 
-let optimize_non_type_induction_scheme kind dep sort ind =
+let optimize_non_type_induction_scheme kind dep sort _ ind =
   let env = Global.env () in
   let sigma = Evd.from_env env in
   if check_scheme kind ind then
@@ -68,15 +68,15 @@ let build_induction_scheme_in_type dep sort ind =
  
 let rect_scheme_kind_from_type =
   declare_individual_scheme_object "_rect_nodep"
-    (fun x -> build_induction_scheme_in_type false InType x, Declareops.no_seff)
+    (fun _ x -> build_induction_scheme_in_type false InType x, Declareops.no_seff)
 
 let rect_scheme_kind_from_prop =
   declare_individual_scheme_object "_rect" ~aux:"_rect_from_prop"
-    (fun x -> build_induction_scheme_in_type false InType x, Declareops.no_seff)
+    (fun _ x -> build_induction_scheme_in_type false InType x, Declareops.no_seff)
 
 let rect_dep_scheme_kind_from_type =
   declare_individual_scheme_object "_rect" ~aux:"_rect_from_type"
-    (fun x -> build_induction_scheme_in_type true InType x, Declareops.no_seff)
+    (fun _ x -> build_induction_scheme_in_type true InType x, Declareops.no_seff)
 
 let ind_scheme_kind_from_type =
   declare_individual_scheme_object "_ind_nodep"
@@ -109,24 +109,24 @@ let build_case_analysis_scheme_in_type dep sort ind =
 
 let case_scheme_kind_from_type =
   declare_individual_scheme_object "_case_nodep"
-  (fun x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff)
+  (fun _ x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff)
 
 let case_scheme_kind_from_prop =
   declare_individual_scheme_object "_case" ~aux:"_case_from_prop"
-  (fun x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff)
+  (fun _ x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff)
 
 let case_dep_scheme_kind_from_type =
   declare_individual_scheme_object "_case" ~aux:"_case_from_type"
-  (fun x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff)
+  (fun _ x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff)
 
 let case_dep_scheme_kind_from_type_in_prop =
   declare_individual_scheme_object "_casep_dep"
-  (fun x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff)
+  (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff)
 
 let case_dep_scheme_kind_from_prop =
   declare_individual_scheme_object "_case_dep"
-  (fun x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff)
+  (fun _ x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff)
 
 let case_dep_scheme_kind_from_prop_in_prop =
   declare_individual_scheme_object "_casep"
-  (fun x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff)
+  (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff)
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 8643fe10f0..f7d3ad5d0a 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -191,7 +191,7 @@ let build_sym_scheme env ind =
 
 let sym_scheme_kind =
   declare_individual_scheme_object "_sym_internal"
-  (fun ind -> 
+  (fun _ ind ->
     let c, ctx = build_sym_scheme (Global.env() (* side-effect! *)) ind in
       (c, ctx), Declareops.no_seff)
 
@@ -262,7 +262,7 @@ let build_sym_involutive_scheme env ind =
 
 let sym_involutive_scheme_kind =
   declare_individual_scheme_object "_sym_involutive"
-  (fun ind -> 
+  (fun _ ind ->
     build_sym_involutive_scheme (Global.env() (* side-effect! *)) ind)
 
 (**********************************************************************)
@@ -650,7 +650,7 @@ let build_r2l_forward_rew_scheme = build_r2l_forward_rew_scheme
 (**********************************************************************)
 let rew_l2r_dep_scheme_kind =
   declare_individual_scheme_object "_rew_r_dep"
-  (fun ind -> build_l2r_rew_scheme true (Global.env()) ind InType)
+  (fun _ ind -> build_l2r_rew_scheme true (Global.env()) ind InType)
 
 (**********************************************************************)
 (* Dependent rewrite from right-to-left in conclusion                 *)
@@ -660,7 +660,7 @@ let rew_l2r_dep_scheme_kind =
 (**********************************************************************)
 let rew_r2l_dep_scheme_kind =
   declare_individual_scheme_object "_rew_dep"
-  (fun ind -> build_r2l_rew_scheme true (Global.env()) ind InType,Declareops.no_seff)
+  (fun _ ind -> build_r2l_rew_scheme true (Global.env()) ind InType,Declareops.no_seff)
 
 (**********************************************************************)
 (* Dependent rewrite from right-to-left in hypotheses                 *)
@@ -670,7 +670,7 @@ let rew_r2l_dep_scheme_kind =
 (**********************************************************************)
 let rew_r2l_forward_dep_scheme_kind =
   declare_individual_scheme_object "_rew_fwd_dep"
-  (fun ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff)
+  (fun _ ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff)
 
 (**********************************************************************)
 (* Dependent rewrite from left-to-right in hypotheses                 *)
@@ -680,7 +680,7 @@ let rew_r2l_forward_dep_scheme_kind =
 (**********************************************************************)
 let rew_l2r_forward_dep_scheme_kind =
   declare_individual_scheme_object "_rew_fwd_r_dep"
-  (fun ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff)
+  (fun _ ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff)
 
 (**********************************************************************)
 (* Non-dependent rewrite from either left-to-right in conclusion or   *)
@@ -693,7 +693,7 @@ let rew_l2r_forward_dep_scheme_kind =
 (**********************************************************************)
 let rew_l2r_scheme_kind =
   declare_individual_scheme_object "_rew_r"
-  (fun ind -> fix_r2l_forward_rew_scheme
+  (fun _ ind -> fix_r2l_forward_rew_scheme
      (build_r2l_forward_rew_scheme false (Global.env()) ind InType), Declareops.no_seff)
 
 (**********************************************************************)
@@ -704,7 +704,7 @@ let rew_l2r_scheme_kind =
 (**********************************************************************)
 let rew_r2l_scheme_kind =
   declare_individual_scheme_object "_rew"
-  (fun ind -> build_r2l_rew_scheme false (Global.env()) ind InType, Declareops.no_seff)
+  (fun _ ind -> build_r2l_rew_scheme false (Global.env()) ind InType, Declareops.no_seff)
 
 (* End of rewriting schemes *)
 
@@ -780,6 +780,6 @@ let build_congr env (eq,refl,ctx) ind =
   in c, Evd.evar_universe_context_of ctx
 
 let congr_scheme_kind = declare_individual_scheme_object "_congr"
-  (fun ind ->
+  (fun _ ind ->
     (* May fail if equality is not defined *)
     build_congr (Global.env()) (get_coq_eq Univ.ContextSet.empty) ind, Declareops.no_seff)
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 16683d243e..118ffb3e80 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -111,7 +111,7 @@ let check_bool_is_defined () =
 
 let beq_scheme_kind_aux = ref (fun _ -> failwith "Undefined")
 
-let build_beq_scheme kn =
+let build_beq_scheme mode kn =
   check_bool_is_defined ();
   (* fetching global env *)
   let env = Global.env() in
@@ -188,7 +188,7 @@ let build_beq_scheme kn =
             else begin
               try
                 let eq, eff =
-                  let c, eff = find_scheme (!beq_scheme_kind_aux()) (kn',i) in
+                  let c, eff = find_scheme ~mode (!beq_scheme_kind_aux()) (kn',i) in
                   mkConst c, eff in
                 let eqa, eff =
                   let eqa, effs = List.split (List.map aux a) in
@@ -330,7 +330,7 @@ let destruct_ind c =
 so from Ai we can find the the correct eq_Ai bl_ai or lb_ai
 *)
 (* used in the leib -> bool side*)
-let do_replace_lb lb_scheme_key aavoid narg p q =
+let do_replace_lb mode lb_scheme_key aavoid narg p q =
   let avoid = Array.of_list aavoid in
   let do_arg v offset =
   try
@@ -360,7 +360,7 @@ let do_replace_lb lb_scheme_key aavoid narg p q =
     let u,v = destruct_ind type_of_pq
     in let lb_type_of_p =
         try
-          let c, eff = find_scheme lb_scheme_key (out_punivs u) (*FIXME*) in
+          let c, eff = find_scheme ~mode lb_scheme_key (out_punivs u) (*FIXME*) in
           Proofview.tclUNIT (mkConst c, eff)
         with Not_found ->
           (* spiwack: the format of this error message should probably
@@ -388,7 +388,7 @@ let do_replace_lb lb_scheme_key aavoid narg p q =
   end
 
 (* used in the bool -> leib side *)
-let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
+let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
   let avoid = Array.of_list aavoid in
   let do_arg v offset =
   try
@@ -551,7 +551,7 @@ let compute_bl_goal ind lnamesparrec nparrec =
               (mkApp(Lazy.force eq,[|mkFullInd (ind,u) (nparrec+3);mkVar n;mkVar m|]))
         ))), eff
 
-let compute_bl_tact bl_scheme_key ind lnamesparrec nparrec =
+let compute_bl_tact mode bl_scheme_key ind lnamesparrec nparrec =
   let list_id = list_id lnamesparrec in
   let avoid = ref [] in
       let first_intros =
@@ -608,7 +608,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
                               if eq_gr (IndRef indeq) Coqlib.glob_eq
                               then
                                 Tacticals.New.tclTHEN
-                                  (do_replace_bl bl_scheme_key ind
+                                  (do_replace_bl mode bl_scheme_key ind
 				     (!avoid)
                                      nparrec (ca.(2))
                                      (ca.(1)))
@@ -625,7 +625,12 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
 
 let bl_scheme_kind_aux = ref (fun _ -> failwith "Undefined")
 
-let make_bl_scheme mind =
+let side_effect_of_mode = function
+  | Declare.KernelVerbose -> false
+  | Declare.KernelSilent -> true
+  | Declare.UserVerbose -> false
+
+let make_bl_scheme mode mind =
   let mib = Global.lookup_mind mind in
   if not (Int.equal (Array.length mib.mind_packets) 1) then
     errorlabstrm ""
@@ -637,8 +642,9 @@ let make_bl_scheme mind =
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
   let bl_goal, eff = compute_bl_goal ind lnamesparrec nparrec in
   let ctx = Evd.empty_evar_universe_context (*FIXME univs *) in
-  let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff:false (Global.env()) ctx bl_goal
-    (compute_bl_tact (!bl_scheme_kind_aux()) (ind, Univ.Instance.empty) lnamesparrec nparrec)
+  let side_eff = side_effect_of_mode mode in
+  let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx bl_goal
+    (compute_bl_tact mode (!bl_scheme_kind_aux()) (ind, Univ.Instance.empty) lnamesparrec nparrec)
   in
   ([|ans|], ctx), eff
 
@@ -688,7 +694,7 @@ let compute_lb_goal ind lnamesparrec nparrec =
               (mkApp(eq,[|bb;mkApp(eqI,[|mkVar n;mkVar m|]);tt|]))
         ))), eff
 
-let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec =
+let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec =
   let list_id = list_id lnamesparrec in
     let avoid = ref [] in
       let first_intros =
@@ -732,7 +738,7 @@ let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec =
                         | App(c,ca) -> (match (kind_of_term ca.(1)) with
                           | App(c',ca') ->
                               let n = Array.length ca' in
-                              do_replace_lb lb_scheme_key
+                              do_replace_lb mode lb_scheme_key
 				(!avoid)
                                 nparrec
                                 ca'.(n-2) ca'.(n-1)
@@ -747,7 +753,7 @@ let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec =
 
 let lb_scheme_kind_aux = ref (fun () -> failwith "Undefined")
 
-let make_lb_scheme mind =
+let make_lb_scheme mode mind =
   let mib = Global.lookup_mind mind in
   if not (Int.equal (Array.length mib.mind_packets) 1) then
     errorlabstrm ""
@@ -759,8 +765,9 @@ let make_lb_scheme mind =
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
   let lb_goal, eff = compute_lb_goal ind lnamesparrec nparrec in
   let ctx = Evd.empty_evar_universe_context in
-  let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff:false (Global.env()) ctx lb_goal
-    (compute_lb_tact (!lb_scheme_kind_aux()) ind lnamesparrec nparrec)
+  let side_eff = side_effect_of_mode mode in
+  let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx lb_goal
+    (compute_lb_tact mode (!lb_scheme_kind_aux()) ind lnamesparrec nparrec)
   in
   ([|ans|], ctx (* FIXME *)), eff
 
@@ -919,7 +926,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
   ]
   end
 
-let make_eq_decidability mind =
+let make_eq_decidability mode mind =
   let mib = Global.lookup_mind mind in
   if not (Int.equal (Array.length mib.mind_packets) 1) then
     raise DecidabilityMutualNotSupported;
@@ -930,7 +937,8 @@ let make_eq_decidability mind =
   let ctx = Evd.empty_evar_universe_context (* FIXME *)in
   let lnonparrec,lnamesparrec =
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
-  let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff:false (Global.env()) ctx
+  let side_eff = side_effect_of_mode mode in
+  let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx
     (compute_dec_goal (ind,u) lnamesparrec nparrec)
     (compute_dec_tact ind lnamesparrec nparrec)
   in
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index 0d39466ede..b59d6fc8ae 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -28,11 +28,10 @@ open Pp
 (**********************************************************************)
 (* Registering schemes in the environment *)
 
-
 type mutual_scheme_object_function =
-  mutual_inductive -> constr array Evd.in_evar_universe_context * Declareops.side_effects
+  internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Declareops.side_effects
 type individual_scheme_object_function =
-  inductive -> constr Evd.in_evar_universe_context * Declareops.side_effects
+  internal_flag -> inductive -> constr Evd.in_evar_universe_context * Declareops.side_effects
 
 type 'a scheme_kind = string
 
@@ -141,32 +140,31 @@ let define internal id c p univs =
   in
   kn
 
-let define_individual_scheme_base kind suff f internal idopt (mind,i as ind) =
-  let (c, ctx), eff = f ind in
+let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) =
+  let (c, ctx), eff = f mode ind in
   let mib = Global.lookup_mind mind in
   let id = match idopt with
     | Some id -> id
     | None -> add_suffix mib.mind_packets.(i).mind_typename suff in
-  let const = define internal id c mib.mind_polymorphic ctx in
+  let const = define mode id c mib.mind_polymorphic ctx in
   declare_scheme kind [|ind,const|];
   const, Declareops.cons_side_effects
      (Safe_typing.sideff_of_scheme kind (Global.safe_env()) [ind,const]) eff
 
-let define_individual_scheme kind internal names (mind,i as ind) =
+let define_individual_scheme kind mode names (mind,i as ind) =
   match Hashtbl.find scheme_object_table kind with
   | _,MutualSchemeFunction f -> assert false
   | s,IndividualSchemeFunction f ->
-      define_individual_scheme_base kind s f internal names ind
+      define_individual_scheme_base kind s f mode names ind
 
-let define_mutual_scheme_base kind suff f internal names mind =
-  let (cl, ctx), eff = f mind in
+let define_mutual_scheme_base kind suff f mode names mind =
+  let (cl, ctx), eff = f mode mind in
   let mib = Global.lookup_mind mind in
   let ids = Array.init (Array.length mib.mind_packets) (fun i ->
       try Int.List.assoc i names
       with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in
-
   let consts = Array.map2 (fun id cl -> 
-     define internal id cl mib.mind_polymorphic ctx) ids cl in
+     define mode id cl mib.mind_polymorphic ctx) ids cl in
   let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in
   declare_scheme kind schemes;
   consts,
@@ -175,11 +173,11 @@ let define_mutual_scheme_base kind suff f internal names mind =
       kind (Global.safe_env()) (Array.to_list schemes))
     eff 
 
-let define_mutual_scheme kind internal names mind =
+let define_mutual_scheme kind mode names mind =
   match Hashtbl.find scheme_object_table kind with
   | _,IndividualSchemeFunction _ -> assert false
   | s,MutualSchemeFunction f ->
-      define_mutual_scheme_base kind s f internal names mind
+      define_mutual_scheme_base kind s f mode names mind
 
 let find_scheme_on_env_too kind ind =
   let s = String.Map.find kind (Indmap.find ind !scheme_map) in
@@ -188,14 +186,14 @@ let find_scheme_on_env_too kind ind =
             kind (Global.safe_env()) [ind, s])
       Declareops.no_seff 
 
-let find_scheme kind (mind,i as ind) =
+let find_scheme ?(mode=KernelSilent) kind (mind,i as ind) =
   try find_scheme_on_env_too kind ind
   with Not_found ->
   match Hashtbl.find scheme_object_table kind with
   | s,IndividualSchemeFunction f ->
-      define_individual_scheme_base kind s f KernelSilent None ind
+      define_individual_scheme_base kind s f mode None ind
   | s,MutualSchemeFunction f ->
-      let ca, eff = define_mutual_scheme_base kind s f KernelSilent [] mind in
+      let ca, eff = define_mutual_scheme_base kind s f mode [] mind in
       ca.(i), eff
 
 let check_scheme kind ind =
diff --git a/toplevel/ind_tables.mli b/toplevel/ind_tables.mli
index 98eaac0928..d0844dd946 100644
--- a/toplevel/ind_tables.mli
+++ b/toplevel/ind_tables.mli
@@ -8,6 +8,7 @@
 
 open Term
 open Names
+open Declare
 
 (** This module provides support for registering inductive scheme builders,
    declaring schemes and generating schemes on demand *)
@@ -19,9 +20,9 @@ type individual
 type 'a scheme_kind
 
 type mutual_scheme_object_function =
-  mutual_inductive -> constr array Evd.in_evar_universe_context * Declareops.side_effects
+  internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Declareops.side_effects
 type individual_scheme_object_function =
-  inductive -> constr Evd.in_evar_universe_context * Declareops.side_effects
+  internal_flag -> inductive -> constr Evd.in_evar_universe_context * Declareops.side_effects
 
 (** Main functions to register a scheme builder *)
 
@@ -32,21 +33,17 @@ val declare_individual_scheme_object : string -> ?aux:string ->
   individual_scheme_object_function ->
   individual scheme_kind
 
-(*
-val declare_scheme : 'a scheme_kind -> (inductive * constant) array -> unit
-*)
-
 (** Force generation of a (mutually) scheme with possibly user-level names *)
 
 val define_individual_scheme : individual scheme_kind -> 
-  Declare.internal_flag (** internal *) ->
+  internal_flag (** internal *) ->
   Id.t option -> inductive -> constant * Declareops.side_effects
 
-val define_mutual_scheme : mutual scheme_kind -> Declare.internal_flag (** internal *) ->
+val define_mutual_scheme : mutual scheme_kind -> internal_flag (** internal *) ->
   (int * Id.t) list -> mutual_inductive -> constant array * Declareops.side_effects
 
 (** Main function to retrieve a scheme in the cache or to generate it *)
-val find_scheme : 'a scheme_kind -> inductive -> constant * Declareops.side_effects
+val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> constant * Declareops.side_effects
 
 val check_scheme : 'a scheme_kind -> inductive -> bool
 
-- 
cgit v1.2.3


From 2ba2ca96be88bad5cd75a02c94cc48ef4f5209b7 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 23 Sep 2015 18:25:15 +0200
Subject: Hopefully better names to constructors of internal_flag, as discussed
 with Enrico.

---
 library/declare.ml        | 10 +++++-----
 library/declare.mli       |  6 +++---
 tactics/extratactics.ml4  |  2 +-
 tactics/rewrite.ml        |  2 +-
 tactics/tactics.ml        |  2 +-
 toplevel/auto_ind_decl.ml |  6 +++---
 toplevel/classes.ml       |  4 ++--
 toplevel/ind_tables.ml    |  8 ++++----
 toplevel/indschemes.ml    | 36 ++++++++++++++++++------------------
 toplevel/record.ml        |  2 +-
 10 files changed, 39 insertions(+), 39 deletions(-)

diff --git a/library/declare.ml b/library/declare.ml
index c3181e4c75..8438380c9c 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -28,9 +28,9 @@ open Decl_kinds
 
 (** flag for internal message display *)
 type internal_flag = 
-  | KernelVerbose (* kernel action, a message is displayed *)
-  | KernelSilent  (* kernel action, no message is displayed *)
-  | UserVerbose   (* user action, a message is displayed *)
+  | UserAutomaticRequest (* kernel action, a message is displayed *)
+  | InternalTacticRequest  (* kernel action, no message is displayed *)
+  | UserIndividualRequest   (* user action, a message is displayed *)
 
 (** Declaration of section variables and local definitions *)
 
@@ -253,7 +253,7 @@ let declare_sideff env fix_exn se =
                if Constant.equal c c' then Some (x,kn) else None) inds_consts)
            knl))
 
-let declare_constant ?(internal = UserVerbose) ?(local = false) id ?(export_seff=false) (cd, kind) =
+let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) =
   let cd = (* We deal with side effects *)
     match cd with
     | Entries.DefinitionEntry de ->
@@ -283,7 +283,7 @@ let declare_constant ?(internal = UserVerbose) ?(local = false) id ?(export_seff
   let kn = declare_constant_common id cst in
   kn
 
-let declare_definition ?(internal=UserVerbose) 
+let declare_definition ?(internal=UserIndividualRequest)
   ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false)
   ?(poly=false) id ?types (body,ctx) =
   let cb = 
diff --git a/library/declare.mli b/library/declare.mli
index d8a00db0cf..76538a6248 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -43,9 +43,9 @@ type constant_declaration = constant_entry * logical_kind
    
    *)
 type internal_flag =
-  | KernelVerbose
-  | KernelSilent
-  | UserVerbose
+  | UserAutomaticRequest
+  | InternalTacticRequest
+  | UserIndividualRequest
 
 (* Defaut definition entries, transparent with no secctx or proj information *)
 val definition_entry : ?opaque:bool -> ?inline:bool -> ?types:types -> 
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index e4240cb5cc..af0870bc92 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -320,7 +320,7 @@ let project_hint pri l2r r =
     Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l"))
   in
   let ctx = Evd.universe_context_set sigma in
-  let c = Declare.declare_definition ~internal:Declare.KernelSilent id (c,ctx) in
+  let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in
     (pri,false,true,Hints.PathAny, Hints.IsGlobRef (Globnames.ConstRef c))
 
 let add_hints_iff l2r lc n bl =
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 3c4550a3cf..c64a1226ab 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1896,7 +1896,7 @@ let add_morphism_infer glob m n =
   let instance = build_morphism_signature m in
   let evd = Evd.empty (*FIXME *) in
     if Lib.is_modtype () then
-      let cst = Declare.declare_constant ~internal:Declare.KernelSilent instance_id
+      let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id
 				(Entries.ParameterEntry 
 				 (None,poly,(instance,Univ.UContext.empty),None), 
 				 Decl_kinds.IsAssumption Decl_kinds.Logical)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index ad7ff14e6b..b113ed31e9 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4450,7 +4450,7 @@ let abstract_subproof id gk tac =
   let cd = Entries.DefinitionEntry const in
   let decl = (cd, IsProof Lemma) in
   (** ppedrot: seems legit to have abstracted subproofs as local*)
-  let cst = Declare.declare_constant ~internal:Declare.KernelSilent ~local:true id decl in
+  let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest ~local:true id decl in
   (* let evd, lem = Evd.fresh_global (Global.env ()) evd (ConstRef cst) in *)
   let lem, ctx = Universes.unsafe_constr_of_global (ConstRef cst) in
   let evd = Evd.set_universe_context evd ectx in
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 118ffb3e80..4122487e23 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -626,9 +626,9 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
 let bl_scheme_kind_aux = ref (fun _ -> failwith "Undefined")
 
 let side_effect_of_mode = function
-  | Declare.KernelVerbose -> false
-  | Declare.KernelSilent -> true
-  | Declare.UserVerbose -> false
+  | Declare.UserAutomaticRequest -> false
+  | Declare.InternalTacticRequest -> true
+  | Declare.UserIndividualRequest -> false
 
 let make_bl_scheme mode mind =
   let mib = Global.lookup_mind mind in
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 33891ad94c..7fe79d948b 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -186,7 +186,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
 	in
 	Evarutil.check_evars env Evd.empty !evars termtype;
 	let ctx = Evd.universe_context !evars in
-	let cst = Declare.declare_constant ~internal:Declare.KernelSilent id
+	let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id
 	  (Entries.ParameterEntry 
             (None,poly,(termtype,ctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical)
 	in instance_hook k None global imps ?hook (ConstRef cst); id
@@ -363,7 +363,7 @@ let context poly l =
     if Lib.is_modtype () && not (Lib.sections_are_opened ()) then
       let uctx = Univ.ContextSet.to_context uctx in	
       let decl = (ParameterEntry (None,poly,(t,uctx),None), IsAssumption Logical) in
-      let cst = Declare.declare_constant ~internal:Declare.KernelSilent id decl in
+      let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in
 	match class_of_constr t with
 	| Some (rels, ((tc,_), args) as _cl) ->
 	    add_instance (Typeclasses.new_instance tc None false (*FIXME*)
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index b59d6fc8ae..218c47b28d 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -113,8 +113,8 @@ let is_visible_name id =
 
 let compute_name internal id =
   match internal with
-  | KernelVerbose | UserVerbose -> id
-  | KernelSilent ->
+  | UserAutomaticRequest | UserIndividualRequest -> id
+  | InternalTacticRequest ->
       Namegen.next_ident_away_from (add_prefix "internal_" id) is_visible_name
 
 let define internal id c p univs =
@@ -135,7 +135,7 @@ let define internal id c p univs =
   } in
   let kn = fd id (DefinitionEntry entry, Decl_kinds.IsDefinition Scheme) in
   let () = match internal with
-    | KernelSilent -> ()
+    | InternalTacticRequest -> ()
     | _-> definition_message id
   in
   kn
@@ -186,7 +186,7 @@ let find_scheme_on_env_too kind ind =
             kind (Global.safe_env()) [ind, s])
       Declareops.no_seff 
 
-let find_scheme ?(mode=KernelSilent) kind (mind,i as ind) =
+let find_scheme ?(mode=InternalTacticRequest) kind (mind,i as ind) =
   try find_scheme_on_env_too kind ind
   with Not_found ->
   match Hashtbl.find scheme_object_table kind with
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index 286d164c42..452d5fbe50 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -146,8 +146,8 @@ let declare_beq_scheme_gen internal names kn =
 let alarm what internal msg =
   let debug = false in
   match internal with
-  | KernelVerbose 
-  | KernelSilent ->
+  | UserAutomaticRequest
+  | InternalTacticRequest ->
     (if debug then
       msg_warning
 	(hov 0 msg ++ fnl () ++ what ++ str " not defined."))
@@ -195,13 +195,13 @@ let beq_scheme_msg mind =
     (List.init (Array.length mib.mind_packets) (fun i -> (mind,i)))
 
 let declare_beq_scheme_with l kn =
-  try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen UserVerbose l kn
+  try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen UserIndividualRequest l kn
 
 let try_declare_beq_scheme kn =
   (* TODO: handle Fix, eventually handle
       proof-irrelevance; improve decidability by depending on decidability
       for the parameters rather than on the bl and lb properties *)
-  try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen KernelVerbose [] kn
+  try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen UserAutomaticRequest [] kn
 
 let declare_beq_scheme = declare_beq_scheme_with []
 
@@ -215,7 +215,7 @@ let declare_one_case_analysis_scheme ind =
        induction scheme, the other ones share the same code with the
        apropriate type *)
   if Sorts.List.mem InType kelim then
-    ignore (define_individual_scheme dep KernelVerbose None ind)
+    ignore (define_individual_scheme dep UserAutomaticRequest None ind)
 
 (* Induction/recursion schemes *)
 
@@ -238,7 +238,7 @@ let declare_one_induction_scheme ind =
     List.map_filter (fun (sort,kind) ->
       if Sorts.List.mem sort kelim then Some kind else None)
       (if from_prop then kinds_from_prop else kinds_from_type) in
-  List.iter (fun kind -> ignore (define_individual_scheme kind KernelVerbose None ind))
+  List.iter (fun kind -> ignore (define_individual_scheme kind UserAutomaticRequest None ind))
     elims
 
 let declare_induction_schemes kn =
@@ -261,11 +261,11 @@ let eq_dec_scheme_msg ind = (* TODO: mutual inductive case *)
 
 let declare_eq_decidability_scheme_with l kn =
   try_declare_scheme (eq_dec_scheme_msg (kn,0))
-    declare_eq_decidability_gen UserVerbose l kn
+    declare_eq_decidability_gen UserIndividualRequest l kn
 
 let try_declare_eq_decidability kn =
   try_declare_scheme (eq_dec_scheme_msg (kn,0))
-    declare_eq_decidability_gen KernelVerbose [] kn
+    declare_eq_decidability_gen UserAutomaticRequest [] kn
 
 let declare_eq_decidability = declare_eq_decidability_scheme_with []
 
@@ -274,17 +274,17 @@ let ignore_error f x =
 
 let declare_rewriting_schemes ind =
   if Hipattern.is_inductive_equality ind then begin
-    ignore (define_individual_scheme rew_r2l_scheme_kind KernelVerbose None ind);
-    ignore (define_individual_scheme rew_r2l_dep_scheme_kind KernelVerbose None ind);
+    ignore (define_individual_scheme rew_r2l_scheme_kind UserAutomaticRequest None ind);
+    ignore (define_individual_scheme rew_r2l_dep_scheme_kind UserAutomaticRequest None ind);
     ignore (define_individual_scheme rew_r2l_forward_dep_scheme_kind
-      KernelVerbose None ind);
+      UserAutomaticRequest None ind);
     (* These ones expect the equality to be symmetric; the first one also *)
     (* needs eq *)
-    ignore_error (define_individual_scheme rew_l2r_scheme_kind KernelVerbose None) ind;
+    ignore_error (define_individual_scheme rew_l2r_scheme_kind UserAutomaticRequest None) ind;
     ignore_error
-      (define_individual_scheme rew_l2r_dep_scheme_kind KernelVerbose None) ind;
+      (define_individual_scheme rew_l2r_dep_scheme_kind UserAutomaticRequest None) ind;
     ignore_error
-      (define_individual_scheme rew_l2r_forward_dep_scheme_kind KernelVerbose None) ind
+      (define_individual_scheme rew_l2r_forward_dep_scheme_kind UserAutomaticRequest None) ind
   end
 
 let declare_congr_scheme ind =
@@ -293,7 +293,7 @@ let declare_congr_scheme ind =
       try Coqlib.check_required_library Coqlib.logic_module_name; true
       with e when Errors.noncritical e -> false
     then
-      ignore (define_individual_scheme congr_scheme_kind KernelVerbose None ind)
+      ignore (define_individual_scheme congr_scheme_kind UserAutomaticRequest None ind)
     else
       msg_warning (strbrk "Cannot build congruence scheme because eq is not found")
   end
@@ -301,7 +301,7 @@ let declare_congr_scheme ind =
 let declare_sym_scheme ind =
   if Hipattern.is_inductive_equality ind then
     (* Expect the equality to be symmetric *)
-    ignore_error (define_individual_scheme sym_scheme_kind KernelVerbose None) ind
+    ignore_error (define_individual_scheme sym_scheme_kind UserAutomaticRequest None) ind
 
 (* Scheme command *)
 
@@ -372,7 +372,7 @@ let do_mutual_induction_scheme lnamedepindsort =
     let decltype = Retyping.get_type_of env0 sigma decl in
     (* let decltype = refresh_universes decltype in *)
     let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Declareops.no_seff) in
-    let cst = define fi UserVerbose sigma proof_output (Some decltype) in
+    let cst = define fi UserIndividualRequest sigma proof_output (Some decltype) in
     ConstRef cst :: lrecref
   in
   let _ = List.fold_right2 declare listdecl lrecnames [] in
@@ -470,7 +470,7 @@ let do_combined_scheme name schemes =
   in
   let body,typ = build_combined_scheme (Global.env ()) csts in
   let proof_output = Future.from_val ((body,Univ.ContextSet.empty),Declareops.no_seff) in
-  ignore (define (snd name) UserVerbose Evd.empty proof_output (Some typ));
+  ignore (define (snd name) UserIndividualRequest Evd.empty proof_output (Some typ));
   fixpoint_message None [snd name]
 
 (**********************************************************************)
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 484fd081df..e214f9ca71 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -298,7 +298,7 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field
 		    const_entry_inline_code = false;
 		    const_entry_feedback = None } in
 		  let k = (DefinitionEntry entry,IsDefinition kind) in
-		  let kn = declare_constant ~internal:KernelSilent fid k in
+		  let kn = declare_constant ~internal:InternalTacticRequest fid k in
 		  let constr_fip =
 		    let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in
 		      applist (mkConstU (kn,u),proj_args) 
-- 
cgit v1.2.3


From b6725a2d0077239e51385a62a526ab9465eea26d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 24 Sep 2015 18:45:40 +0200
Subject: The -compile option now accepts ".v" files and outputs a warning
 otherwise.

---
 library/library.ml  | 12 ++++++------
 library/library.mli | 10 ++++++----
 toplevel/vernac.ml  | 16 +++++++++++++---
 3 files changed, 25 insertions(+), 13 deletions(-)

diff --git a/library/library.ml b/library/library.ml
index f7ca4e9760..1bcffcd147 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -678,22 +678,22 @@ let check_module_name s =
     | c -> err c
 
 let start_library f =
-  let paths = Loadpath.get_paths () in
-  let _, longf =
-    System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in
+  let () = if not (Sys.file_exists f) then
+    errorlabstrm "" (hov 0 (str "Can't find file" ++ spc () ++ str f))
+  in
   let ldir0 =
     try
-      let lp = Loadpath.find_load_path (Filename.dirname longf) in
+      let lp = Loadpath.find_load_path (Filename.dirname f) in
       Loadpath.logical lp
     with Not_found -> Nameops.default_root_prefix
   in
-  let file = Filename.basename f in
+  let file = Filename.chop_extension (Filename.basename f) in
   let id = Id.of_string file in
   check_module_name file;
   check_coq_overwriting ldir0 id;
   let ldir = add_dirpath_suffix ldir0 id in
   Declaremods.start_library ldir;
-  ldir,longf
+  ldir
 
 let load_library_todo f =
   let paths = Loadpath.get_paths () in
diff --git a/library/library.mli b/library/library.mli
index 967a54e4c8..f2e60718d6 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -25,7 +25,7 @@ val require_library_from_dirpath : (DirPath.t * string) list -> bool option -> u
 val require_library_from_file :
   Id.t option -> CUnix.physical_path -> bool option -> unit
 
-(** {6 ... } *)
+(** {6 Start the compilation of a library } *)
 
 (** Segments of a library *)
 type seg_sum
@@ -39,10 +39,12 @@ type seg_proofs = Term.constr Future.computation array
    an export otherwise just a simple import *)
 val import_module : bool -> qualid located list -> unit
 
-(** {6 Start the compilation of a library } *)
-val start_library : string -> DirPath.t * string
+(** Start the compilation of a file as a library. The argument must be an
+    existing file on the system, and the returned path is the associated
+    absolute logical path of the library. *)
+val start_library : CUnix.physical_path -> DirPath.t
 
-(** {6 End the compilation of a library and save it to a ".vo" file } *)
+(** End the compilation of a library and save it to a ".vo" file *)
 val save_library_to :
   ?todo:(((Future.UUID.t,'document) Stateid.request * bool) list * 'counters) ->
   DirPath.t -> string -> Opaqueproof.opaquetab -> unit
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 266d8f9b4f..14d2bcea41 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -294,7 +294,15 @@ let load_vernac verb file =
     if !Flags.beautify_file then close_out !chan_beautify;
     raise_with_file file (disable_drop e, info)
 
-(* Compile a vernac file (f is assumed without .v suffix) *)
+let ensure_v f =
+  if Filename.check_suffix f ".v" then f
+  else begin
+    msg_warning (str "File \"" ++ str f ++ strbrk "\" has been implicitly \
+    expanded to \"" ++ str f ++ str ".v\"");
+    f ^ ".v"
+  end
+
+(* Compile a vernac file *)
 let compile verbosely f =
   let check_pending_proofs () =
     let pfs = Pfedit.get_all_proof_names () in
@@ -302,7 +310,8 @@ let compile verbosely f =
       (msg_error (str "There are pending proofs"); flush_all (); exit 1) in
   match !Flags.compilation_mode with
   | BuildVo ->
-      let ldir,long_f_dot_v = Flags.verbosely Library.start_library f in
+      let long_f_dot_v = ensure_v f in
+      let ldir = Flags.verbosely Library.start_library long_f_dot_v in
       Stm.set_compilation_hints long_f_dot_v;
       Aux_file.start_aux_file_for long_f_dot_v;
       Dumpglob.start_dump_glob long_f_dot_v;
@@ -318,7 +327,8 @@ let compile verbosely f =
       Aux_file.stop_aux_file ();
       Dumpglob.end_dump_glob ()
   | BuildVio ->
-      let ldir, long_f_dot_v = Flags.verbosely Library.start_library f in
+      let long_f_dot_v = ensure_v f in
+      let ldir = Flags.verbosely Library.start_library long_f_dot_v in
       Dumpglob.noglob ();
       Stm.set_compilation_hints long_f_dot_v;
       let _ = load_vernac verbosely long_f_dot_v in
-- 
cgit v1.2.3


From 3930c586507bfb3b80297d7a2fdbbc6049aa509b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 24 Sep 2015 19:13:30 +0200
Subject: Updating the documentation and the toolchain w.r.t. the change in
 -compile.

---
 CHANGES                   | 3 +++
 Makefile.build            | 4 ++--
 doc/refman/RefMan-com.tex | 4 ++--
 man/coqtop.1              | 4 ++--
 test-suite/Makefile       | 6 +++---
 tools/coqc.ml             | 7 +------
 toplevel/usage.ml         | 4 ++--
 7 files changed, 15 insertions(+), 17 deletions(-)

diff --git a/CHANGES b/CHANGES
index c8fca217fd..e3224db048 100644
--- a/CHANGES
+++ b/CHANGES
@@ -51,6 +51,9 @@ Tools
 - Flag -no-native-compiler was removed and became the default for coqc. If
   precompilation of files for native conversion test is desired, use
   -native-compiler.
+- The -compile command-line option now takes the full path of the considered
+  file, including the ".v" extension, and outputs a warning if such an extension
+  is lacking.
 
 Changes from V8.5beta1 to V8.5beta2
 ===================================
diff --git a/Makefile.build b/Makefile.build
index 6ceff2de95..39f60bd595 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -587,7 +587,7 @@ pluginsbyte: $(PLUGINS)
 theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_DEP) | theories/Init/%.v.d
 	$(SHOW)'COQC -noinit $<'
 	$(HIDE)rm -f theories/Init/$*.glob
-	$(HIDE)$(BOOTCOQC) theories/Init/$* -noinit -R theories Coq
+	$(HIDE)$(BOOTCOQC) $< -noinit -R theories Coq
 
 theories/Numbers/Natural/BigN/NMake_gen.v: theories/Numbers/Natural/BigN/NMake_gen.ml
 	$(OCAML) $< $(TOTARGET)
@@ -1038,7 +1038,7 @@ plugins/%_mod.ml: plugins/%.mllib
 %.vo %.glob: %.v theories/Init/Prelude.vo $(VO_TOOLS_DEP) | %.v.d
 	$(SHOW)'COQC      $<'
 	$(HIDE)rm -f $*.glob 
-	$(HIDE)$(BOOTCOQC) $*
+	$(HIDE)$(BOOTCOQC) $<
 ifdef VALIDATE
 	$(SHOW)'COQCHK    $(call vo_to_mod,$@)'
 	$(HIDE)$(CHICKEN) -boot -silent -norec $(call vo_to_mod,$@) \
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 6335dfd324..2f9758fdee 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -162,11 +162,11 @@ Add physical path {\em directory} to the {\ocaml} loadpath.
   Load \Coq~compiled file {\em file}{\tt .vo} and import it ({\tt
     Require} {\em file}).
 
-\item[{\tt -compile} {\em file},{\tt -compile-verbose} {\em file}, {\tt -batch}]\ 
+\item[{\tt -compile} {\em file.v},{\tt -compile-verbose} {\em file.v}, {\tt -batch}]\ 
 
   {\tt coqtop} options only used internally by {\tt coqc}.
 
-  This compiles file {\em file}{\tt .v} into {\em file}{\tt .vo} without/with a
+  This compiles file {\em file.v} into {\em file}{\tt .vo} without/with a
   copy of the contents of the file on standard input.  This option implies options
   {\tt -batch} (exit just after arguments parsing). It is only
   available for {\tt coqtop}.
diff --git a/man/coqtop.1 b/man/coqtop.1
index 1bc4629d0f..705ea43f67 100644
--- a/man/coqtop.1
+++ b/man/coqtop.1
@@ -84,7 +84,7 @@ load Coq object file
 and import it (Require Import filename.)
 
 .TP
-.BI \-compile \ filename
+.BI \-compile \ filename.v
 compile Coq file
 .I filename.v 
 (implies 
@@ -92,7 +92,7 @@ compile Coq file
 )
 
 .TP
-.BI \-compile\-verbose \ filename
+.BI \-compile\-verbose \ filename.v
 verbosely compile Coq file
 .I filename.v
 (implies 
diff --git a/test-suite/Makefile b/test-suite/Makefile
index d2466250ab..39c36d5414 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -208,7 +208,7 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
-	  $(coqc) "$*" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
+	  $(coqc) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
 	  if [ $$R != 0 ]; then \
 	    echo $(log_failure); \
 	    echo "    $<...could not be prepared" ; \
@@ -238,7 +238,7 @@ $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
-	  $(coqc) "$*" $(call get_coq_prog_args,"$<") -async-proofs on \
+	  $(coqc) "$<" $(call get_coq_prog_args,"$<") -async-proofs on \
 	    -async-proofs-private-flags fallback-to-lazy-if-marshal-error=no,fallback-to-lazy-if-slave-dies=no \
 	    $$opts 2>&1; R=$$?; times; \
 	  if [ $$R = 0 ]; then \
@@ -352,7 +352,7 @@ $(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v
 # Additionnal dependencies for module tests
 $(addsuffix .log,$(wildcard modules/*.v)): %.v.log: modules/Nat.vo modules/plik.vo
 modules/%.vo: modules/%.v
-	$(HIDE)$(coqtop) -R modules Mods -compile $(<:.v=)
+	$(HIDE)$(coqtop) -R modules Mods -compile $<
 
 #######################################################################
 # Miscellaneous tests
diff --git a/tools/coqc.ml b/tools/coqc.ml
index 5710b97f2a..e7239da682 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -30,13 +30,8 @@ let verbose = ref false
 let rec make_compilation_args = function
   | [] -> []
   | file :: fl ->
-      let file_noext =
-        if Filename.check_suffix file ".v" then
-          Filename.chop_suffix file ".v"
-        else file
-      in
       (if !verbose then "-compile-verbose" else "-compile")
-      :: file_noext :: (make_compilation_args fl)
+      :: file :: (make_compilation_args fl)
 
 (* compilation of files [files] with command [command] and args [args] *)
 
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index a5d8450b9d..3c001eadcc 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -43,8 +43,8 @@ let print_usage_channel co command =
 \n  -lv f	                 (idem)\
 \n  -load-vernac-object f  load Coq object file f.vo\
 \n  -require f             load Coq object file f.vo and import it (Require f.)\
-\n  -compile f             compile Coq file f.v (implies -batch)\
-\n  -compile-verbose f     verbosely compile Coq file f.v (implies -batch)\
+\n  -compile f.v           compile Coq file f.v (implies -batch)\
+\n  -compile-verbose f.v   verbosely compile Coq file f.v (implies -batch)\
 \n  -quick                 quickly compile .v files to .vio files (skip proofs)\
 \n  -schedule-vio2vo j f1..fn   run up to j instances of Coq to turn each fi.vio\
 \n                         into fi.vo\
-- 
cgit v1.2.3


From 8e25e107a8715728a7227934d7b11035863ee5f0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 25 Sep 2015 12:25:35 +0200
Subject: The -require option now accepts a logical path instead of a physical
 one.

---
 CHANGES                    |  2 ++
 doc/refman/RefMan-com.tex  |  6 +++---
 library/library.ml         | 20 +++++---------------
 library/library.mli        |  3 +--
 man/coqide.1               | 10 +++++-----
 man/coqtop.1               |  8 ++++----
 toplevel/coqtop.ml         |  8 ++++----
 toplevel/usage.ml          |  2 +-
 toplevel/vernacentries.mli |  3 +++
 9 files changed, 28 insertions(+), 34 deletions(-)

diff --git a/CHANGES b/CHANGES
index e3224db048..950f2fab18 100644
--- a/CHANGES
+++ b/CHANGES
@@ -54,6 +54,8 @@ Tools
 - The -compile command-line option now takes the full path of the considered
   file, including the ".v" extension, and outputs a warning if such an extension
   is lacking.
+- The -require command-line option now takes a logical path of a given library
+  rather than a physical path.
 
 Changes from V8.5beta1 to V8.5beta2
 ===================================
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 2f9758fdee..0f1823a021 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -157,10 +157,10 @@ Add physical path {\em directory} to the {\ocaml} loadpath.
 
   Load \Coq~compiled file {\em file}{\tt .vo}
 
-\item[{\tt -require} {\em file}]\ 
+\item[{\tt -require} {\em path}]\ 
 
-  Load \Coq~compiled file {\em file}{\tt .vo} and import it ({\tt
-    Require} {\em file}).
+  Load \Coq~compiled library {\em path} and import it (equivalent to {\tt
+    Require Import} {\em path}).
 
 \item[{\tt -compile} {\em file.v},{\tt -compile-verbose} {\em file.v}, {\tt -batch}]\ 
 
diff --git a/library/library.ml b/library/library.ml
index 1bcffcd147..a09f91b15a 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -488,18 +488,8 @@ let rec_intern_library libs mref =
   let _, libs = intern_library libs mref None in
   libs
 
-let check_library_short_name f dir = function
-  | Some id when not (Id.equal id (snd (split_dirpath dir))) ->
-      errorlabstrm "check_library_short_name"
-      (str "The file " ++ str f ++ str " contains library" ++ spc () ++
-      pr_dirpath dir ++ spc () ++ str "and not library" ++ spc () ++
-      pr_id id)
-  | _ -> ()
-
-let rec_intern_by_filename_only id f =
+let rec_intern_by_filename_only f =
   let m = try intern_from_file f with Sys_error s -> error s in
-  (* Only the base name is expected to match *)
-  check_library_short_name f m.library_name id;
   (* We check no other file containing same library is loaded *)
   if library_is_loaded m.library_name then
     begin
@@ -518,12 +508,12 @@ let native_name_from_filename f =
   let (lmd : seg_sum), pos, digest_lmd = System.marshal_in_segment f ch in
   Nativecode.mod_uid_of_dirpath lmd.md_name
 
-let rec_intern_library_from_file idopt f =
+let rec_intern_library_from_file f =
   (* A name is specified, we have to check it contains library id *)
   let paths = Loadpath.get_paths () in
   let _, f =
     System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".vo") in
-  rec_intern_by_filename_only idopt f
+  rec_intern_by_filename_only f
 
 (**********************************************************************)
 (*s [require_library] loads and possibly opens a library. This is a
@@ -600,8 +590,8 @@ let require_library_from_dirpath modrefl export =
       add_anonymous_leaf (in_require (needed,modrefl,export));
   add_frozen_state ()
 
-let require_library_from_file idopt file export =
-  let modref,needed = rec_intern_library_from_file idopt file in
+let require_library_from_file file export =
+  let modref,needed = rec_intern_library_from_file file in
   let needed = List.rev_map snd needed in
   if Lib.is_module_or_modtype () then begin
     add_anonymous_leaf (in_require (needed,[modref],None));
diff --git a/library/library.mli b/library/library.mli
index f2e60718d6..3d96f9a751 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -22,8 +22,7 @@ open Libnames
 (** Require = load in the environment + open (if the optional boolean
     is not [None]); mark also for export if the boolean is [Some true] *)
 val require_library_from_dirpath : (DirPath.t * string) list -> bool option -> unit
-val require_library_from_file :
-  Id.t option -> CUnix.physical_path -> bool option -> unit
+val require_library_from_file : CUnix.physical_path -> bool option -> unit
 
 (** {6 Start the compilation of a library } *)
 
diff --git a/man/coqide.1 b/man/coqide.1
index 3fa7f0e418..cfd9c3b4a2 100644
--- a/man/coqide.1
+++ b/man/coqide.1
@@ -67,11 +67,11 @@ Load Coq file
 Load Coq object file
 .IR f .vo.
 .TP
-.BI \-require\  f
-Load Coq object file
-.IR f .vo
-and import it (Require
-.IR f .).
+.BI \-require\  path
+Load Coq library
+.IR path
+and import it (Require Import
+.IR path .).
 .TP
 .BI \-compile\  f
 Compile Coq file
diff --git a/man/coqtop.1 b/man/coqtop.1
index 705ea43f67..e079bee39b 100644
--- a/man/coqtop.1
+++ b/man/coqtop.1
@@ -78,10 +78,10 @@ load Coq object file
 .I filename.vo
 
 .TP
-.BI \-require \ filename
-load Coq object file
-.I filename.vo
-and import it (Require Import filename.)
+.BI \-require \ path
+load Coq library
+.I path
+and import it (Require Import path.)
 
 .TP
 .BI \-compile \ filename.v
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index d67559d77f..32ac9a496d 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -171,7 +171,7 @@ let load_vernacular () =
 let load_vernacular_obj = ref ([] : string list)
 let add_vernac_obj s = load_vernacular_obj := s :: !load_vernacular_obj
 let load_vernac_obj () =
-  List.iter (fun f -> Library.require_library_from_file None f None)
+  List.iter (fun f -> Library.require_library_from_file f None)
     (List.rev !load_vernacular_obj)
 
 let require_prelude () =
@@ -185,9 +185,9 @@ let require_prelude () =
 let require_list = ref ([] : string list)
 let add_require s = require_list := s :: !require_list
 let require () =
-  if !load_init then silently require_prelude ();
-  List.iter (fun s -> Library.require_library_from_file None s (Some false))
-    (List.rev !require_list)
+  let () = if !load_init then silently require_prelude () in
+  let map dir = Qualid (Loc.ghost, qualid_of_string dir) in
+  Vernacentries.vernac_require None (Some false) (List.rev_map map !require_list)
 
 let compile_list = ref ([] : (bool * string) list)
 
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 3c001eadcc..472503ced2 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -42,7 +42,7 @@ let print_usage_channel co command =
 \n  -load-vernac-source-verbose f  load Coq file f.v (Load Verbose f.)\
 \n  -lv f	                 (idem)\
 \n  -load-vernac-object f  load Coq object file f.vo\
-\n  -require f             load Coq object file f.vo and import it (Require f.)\
+\n  -require path          load Coq library path and import it (Require Import path.)\
 \n  -compile f.v           compile Coq file f.v (implies -batch)\
 \n  -compile-verbose f.v   verbosely compile Coq file f.v (implies -batch)\
 \n  -quick                 quickly compile .v files to .vio files (skip proofs)\
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index 4b1cd7a013..c6d87596dc 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.mli
@@ -16,6 +16,9 @@ val show_prooftree : unit -> unit
 
 val show_node : unit -> unit
 
+val vernac_require :
+  Libnames.reference option -> bool option -> Libnames.reference list -> unit
+
 (** This function can be used by any command that want to observe terms
    in the context of the current goal *)
 val get_current_context_of_args : int option -> Evd.evar_map * Environ.env
-- 
cgit v1.2.3