Merge branch 'v8.6'

Author: ppedrot

CHANGES

@@ -50,9 +50,10 @@ Tactics
 - Every generic argument type declares a tactic scope of the form "name:(...)"
   where name is the name of the argument. This generalizes the constr: and ltac:
   instances.
-- When in strict mode (i.e. in a Ltac definition) the "intro" tactic cannot use
-  a locally free identifier anymore. It must use e.g. the "fresh" primitive
-  instead (potential source of incompatibilities).
+- When in strict mode (i.e. in a Ltac definition), if the "intro" tactic is
+  given a free identifier, it is not bound in subsequent tactics anymore.
+  In order to introduce a binding, use e.g. the "fresh" primitive instead
+  (potential source of incompatibilities).
 - New tactics is_ind, is_const, is_proj, is_constructor for use in Ltac (DOC TODO).
 - New goal selectors.  Sets of goals can be selected by select by listing
   integers ranges. Example: "1,4-7,24: tac" focuses "tac" on goals 1,4,5,6,7,24.
@@ -61,6 +62,10 @@ Tactics
   "Structural Injection". In this case, hypotheses are also put in the
   context in the natural left-to-right order and the hypothesis on
   which injection applies is cleared.
+- Tactic "contradiction" (hence "easy") now also solve goals with
+  hypotheses of the form "~True" or "t<>t" (possible source of
+  incompatibilities because of more successes in automation, but
+  generally a more intuitive strategy).
 
 Hints
 

doc/refman/RefMan-tac.tex

@@ -1491,10 +1491,10 @@ \subsection{\tt contradiction}
 \tacindex{contradiction}
 
 This tactic applies to any goal. The {\tt contradiction} tactic
-attempts to find in the current context (after all {\tt intros}) one
-hypothesis that is equivalent to {\tt False}. It permits to prune
-irrelevant cases. This tactic is a macro for the tactics sequence
-{\tt intros; elimtype False; assumption}.
+attempts to find in the current context (after all {\tt intros}) an
+hypothesis that is equivalent to an empty inductive type (e.g. {\tt
+  False}), to the negation of a singleton inductive type (e.g. {\tt
+  True} or {\tt x=x}), or two contradictory hypotheses.
 
 \begin{ErrMsgs}
 \item \errindex{No such assumption}

doc/refman/RefMan-uti.tex

@@ -102,7 +102,7 @@
 
 This command generates a file \texttt{Makefile} that can be used to
 compile all the sources of the current project. It follows the
-syntax described by the output of \texttt{\% coq\_makefile ----help}.
+syntax described by the output of \texttt{\% coq\_makefile -{}-help}.
 Once the \texttt{Makefile} file has been generated a first time, it
 can be used by the \texttt{make} command to compile part or all of
 the project. Note that once it has been generated once, as soon as
@@ -112,8 +112,8 @@
 The following command generates a minimal example of
 \texttt{\_CoqProject} file:
 \begin{quotation}
-\texttt{\% \{ echo '-R .} \textit{MyFancyLib} \texttt{' ; find . -name
-  '*.v' -print \} > \_CoqProject}
+\texttt{\% ( echo "-R .\ }\textit{MyFancyLib}\texttt{" ; find .\ -name
+  "*.v" -print ) > \_CoqProject}
 \end{quotation}
 when executed at the root of the directory containing the
 project. Here the \texttt{\_CoqProject} lists all the \texttt{.v} files

engine/proofview.ml

@@ -1058,6 +1058,26 @@ module Goal = struct
     end
     end
 
+  exception NotExactlyOneSubgoal
+  let _ = CErrors.register_handler begin function
+  | NotExactlyOneSubgoal ->
+      CErrors.user_err (Pp.str"Not exactly one subgoal.")
+  | _ -> raise CErrors.Unhandled
+  end
+
+  let enter_one f =
+    let open Proof in
+    Comb.get >>= function
+    | [goal] -> begin
+       Env.get >>= fun env ->
+       tclEVARMAP >>= fun sigma ->
+       try f.enter (gmake env sigma goal)
+       with e when catchable_exception e ->
+         let (e, info) = CErrors.push e in
+         tclZERO ~info e
+      end
+    | _ -> tclZERO NotExactlyOneSubgoal
+
   type ('a, 'b) s_enter =
     { s_enter : 'r. ('a, 'r) t -> ('b, 'r) Sigma.sigma }
 

engine/proofview.mli

@@ -499,6 +499,10 @@ module Goal : sig
   (** Like {!nf_enter}, but does not normalize the goal beforehand. *)
   val enter : ([ `LZ ], unit tactic) enter -> unit tactic
 
+  (** Like {!enter}, but assumes exactly one goal under focus, raising *)
+  (** an error otherwise. *)
+  val enter_one : ([ `LZ ], 'a tactic) enter -> 'a tactic
+
   type ('a, 'b) s_enter =
     { s_enter : 'r. ('a, 'r) t -> ('b, 'r) Sigma.sigma }
 

interp/constrintern.ml

@@ -33,10 +33,10 @@ open Context.Rel.Declaration
 
 (** constr_expr -> glob_constr translation:
     - it adds holes for implicit arguments
-    - it remplaces notations by their value (scopes stuff are here)
+    - it replaces notations by their value (scopes stuff are here)
     - it recognizes global vars from local ones
-    - it prepares pattern maching problems (a pattern becomes a tree where nodes
-    are constructor/variable pairs and leafs are variables)
+    - it prepares pattern matching problems (a pattern becomes a tree
+      where nodes are constructor/variable pairs and leafs are variables)
 
     All that at once, fasten your seatbelt!
 *)

interp/dumpglob.ml

@@ -45,10 +45,10 @@ let dump_string s =
   if dump () && !glob_output != Feedback then 
     Pervasives.output_string !glob_file s
 
-let start_dump_glob vfile =
+let start_dump_glob ~vfile ~vofile =
   match !glob_output with
   | MultFiles ->
-      open_glob_file (Filename.chop_extension vfile ^ ".glob");
+      open_glob_file (Filename.chop_extension vofile ^ ".glob");
       output_string !glob_file "DIGEST ";
       output_string !glob_file (Digest.to_hex (Digest.file vfile));
       output_char !glob_file '\n'

interp/dumpglob.mli

@@ -9,7 +9,7 @@
 val open_glob_file : string -> unit
 val close_glob_file : unit -> unit
 
-val start_dump_glob : string -> unit
+val start_dump_glob : vfile:string -> vofile:string -> unit
 val end_dump_glob : unit -> unit
 
 val dump : unit -> bool

interp/notation_ops.ml

@@ -125,7 +125,7 @@ let rec cases_pattern_fold_map loc g e = function
       e', PatCstr (loc,cstr,patl',na')
 
 let subst_binder_type_vars l = function
-  | Evar_kinds.BinderType (Name id) as e ->
+  | Evar_kinds.BinderType (Name id) ->
      let id =
        try match Id.List.assoc id l with GVar(_,id') -> id' | _ -> id
        with Not_found -> id in

library/lib.ml

@@ -501,13 +501,6 @@ let section_instance = function
 let is_in_section ref =
   try ignore (section_instance ref); true with Not_found -> false
 
-let full_replacement_context () = List.map pi2 !sectab
-let full_section_segment_of_constant con =
-  List.map (fun (vars,_,(x,_)) -> fun hyps ->
-    named_of_variable_context
-      (try pi1 (Names.Cmap.find con x)
-       with Not_found -> fst (extract_hyps (vars, hyps)))) !sectab
-
 (*************)
 (* Sections. *)
 
@@ -608,15 +601,6 @@ let rec dp_of_mp = function
   |Names.MPbound _ -> library_dp ()
   |Names.MPdot (mp,_) -> dp_of_mp mp
 
-let rec split_mp = function
-  |Names.MPfile dp -> dp, Names.DirPath.empty
-  |Names.MPdot (prfx, lbl) ->
-    let mprec, dprec = split_mp prfx in
-    mprec, Libnames.add_dirpath_suffix dprec (Names.Label.to_id lbl)
-  |Names.MPbound mbid ->
-    let (_,id,dp) = Names.MBId.repr mbid in
-    library_dp (), Names.DirPath.make [id]
-
 let rec split_modpath = function
   |Names.MPfile dp -> dp, []
   |Names.MPbound mbid -> library_dp (), [Names.MBId.to_id mbid]
@@ -628,20 +612,6 @@ let library_part = function
   |VarRef id -> library_dp ()
   |ref -> dp_of_mp (mp_of_global ref)
 
-let remove_section_part ref =
-  let sp = Nametab.path_of_global ref in
-  let dir,_ = repr_path sp in
-  match ref with
-  | VarRef id ->
-      anomaly (Pp.str "remove_section_part not supported on local variables")
-  | _ ->
-      if is_dirpath_prefix_of dir (cwd ()) then
-        (* Not yet (fully) discharged *)
-        pop_dirpath_n (sections_depth ()) (cwd ())
-      else
-	(* Theorem/Lemma outside its outer section of definition *)
-	dir
-
 (************************)
 (* Discharging names *)