Merge branch 'v8.5' into trunk

26 files changed, 85 insertions, 45 deletions

diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 473b8dc82e..973ff0b778 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -285,7 +285,7 @@ let default_logger level message =
 
 (** {6 File operations} *)
 
-(** A customized [stat] function. Exceptions are catched. *)
+(** A customized [stat] function. Exceptions are caught. *)
 
 type stats = MTime of float | NoSuchFile | OtherError
 
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index 8269582dfe..c2b51dd396 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -71,7 +71,7 @@ val default_logger : Pp.message_level -> string -> unit
 
 (** {6 I/O operations} *)
 
-(** A customized [stat] function. Exceptions are catched. *)
+(** A customized [stat] function. Exceptions are caught. *)
 
 type stats = MTime of float | NoSuchFile | OtherError
 val stat : string -> stats
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index d6c160c3dd..3b0c93b322 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -38,7 +38,7 @@ open Pre_env
 (* In the function body [arg1] is represented by de Bruijn [n], and       *)
 (* [argn] by de Bruijn [1]                                                *)
 
-(* Representation of environements of mutual fixpoints :                  *)
+(* Representation of environments of mutual fixpoints :                  *)
 (* [t1|C1| ... |tc|Cc| ... |t(nbr)|C(nbr)| fv1 | fv2 | .... | fvn | type] *)
 (*                ^<----------offset--------->                            *)
 (* type = [Ct1 | .... | Ctn]                                              *)
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 65d1de7e11..d762a246e6 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -823,7 +823,7 @@ let retroknowledge f senv =
 let register field value by_clause senv =
   (* todo : value closed, by_clause safe, by_clause of the proper type*)
   (* spiwack : updates the safe_env with the information that the register
-     action has to be performed (again) when the environement is imported *)
+     action has to be performed (again) when the environment is imported *)
   { senv with
     env = Environ.register senv.env field value;
     local_retroknowledge =
diff --git a/kernel/uint31.ml b/kernel/uint31.ml
index 3a0da2f621..d9c723c243 100644
--- a/kernel/uint31.ml
+++ b/kernel/uint31.ml
@@ -1,7 +1,7 @@
   (* Invariant: For arch64 all extra bytes are set to 0 *)
 type t = int 
     
-  (* to be used only on 32 bits achitectures *)
+  (* to be used only on 32 bits architectures *)
 let maxuint31 = Int32.of_string "0x7FFFFFFF"
 let uint_32 i =  Int32.logand (Int32.of_int i) maxuint31
     
@@ -16,7 +16,7 @@ let of_int_64 i = i land 0x7FFFFFFF
 let of_int = select of_int_32 of_int_64
 let of_uint i = i
  	
-    (* convertion of an uint31 to a string *)
+    (* conversion of an uint31 to a string *)
 let to_string_32 i = Int32.to_string (uint_32 i)
 let to_string_64 = string_of_int 
 
diff --git a/kernel/uint31.mli b/kernel/uint31.mli
index e8b980809d..d1f933cc4e 100644
--- a/kernel/uint31.mli
+++ b/kernel/uint31.mli
@@ -5,7 +5,7 @@ val to_int : t -> int
 val of_int : int -> t
 val of_uint : int -> t
 
-     (* convertion to a string *)
+     (* conversion to a string *)
 val to_string : t -> string
 val of_string : string -> t
 
diff --git a/lib/errors.ml b/lib/errors.ml
index ab331d6a4d..a4ec357ee4 100644
--- a/lib/errors.ml
+++ b/lib/errors.ml
@@ -108,7 +108,7 @@ let _ = register_handler begin function
   | _ -> raise Unhandled
 end
 
-(** Critical exceptions shouldn't be catched and ignored by mistake
+(** Critical exceptions should not be caught and ignored by mistake
     by inner functions during a [vernacinterp]. They should be handled
     only at the very end of interp, to be displayed to the user. *)
 
diff --git a/lib/errors.mli b/lib/errors.mli
index e4096a7ef8..03caa6a9f8 100644
--- a/lib/errors.mli
+++ b/lib/errors.mli
@@ -81,7 +81,7 @@ val iprint : Exninfo.iexn -> Pp.std_ppcmds
     isn't printed (used in Ltac debugging). *)
 val print_no_report : exn -> Pp.std_ppcmds
 
-(** Critical exceptions shouldn't be catched and ignored by mistake
+(** Critical exceptions should not be caught and ignored by mistake
     by inner functions during a [vernacinterp]. They should be handled
     only in [Toplevel.do_vernac] (or Ideslave), to be displayed to the user.
     Typical example: [Sys.Break], [Assert_failure], [Anomaly] ...
diff --git a/library/assumptions.mli b/library/assumptions.mli
index 809e536b43..bb36a97259 100644
--- a/library/assumptions.mli
+++ b/library/assumptions.mli
@@ -27,7 +27,7 @@ module ContextObjectMap : Map.ExtS
 (** Collects all the objects on which a term directly relies, bypassing kernel
     opacity, together with the recursive dependence DAG of objects.
 
-    WARNING: some terms may not make sense in the environement, because they are
+    WARNING: some terms may not make sense in the environment, because they are
     sealed inside opaque modules. Do not try to do anything fancy with those
     terms apart from printing them, otherwise demons may fly out of your nose.
 *)
diff --git a/library/library.ml b/library/library.ml
index e4169d66e0..95b817d0a1 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -587,8 +587,11 @@ let import_module export modl =
     | [] -> ()
     | modl -> add_anonymous_leaf (in_import_library (List.rev modl, export)) in
   let rec aux acc = function
-    | m :: l ->
-        (match safe_locate_module m with
+    | (loc,dir as m) :: l ->
+        let m,acc =
+          try Nametab.locate_module dir, acc
+          with Not_found-> flush acc; safe_locate_module m, [] in
+        (match m with
         | MPfile dir -> aux (dir::acc) l
         | mp -> flush acc; Declaremods.import_module export mp; aux [] l)
     | [] -> flush acc
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index a2577e2b0a..f6a543a1c6 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -252,7 +252,7 @@ let coq_False_ref =
 
 (*
   [make_discr_match_el \[e1,...en\]] builds match e1,...,en with
-  (the list of expresions on which we will do the matching)
+  (the list of expressions on which we will do the matching)
  *)
 let make_discr_match_el  =
   List.map (fun e -> (e,(Anonymous,None)))
@@ -674,7 +674,7 @@ and build_entry_lc_from_case env funname make_discr
 	   match el with brl end
 	   we first compute the list of lists corresponding to [el] and
 	   combine them .
-	   Then for each elemeent of the combinations,
+	   Then for each element of the combinations,
 	   we compute the result we compute one list per branch in [brl] and
 	   finally we just concatenate those list
 	*)
@@ -720,9 +720,9 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
   match brl with
     | [] -> (* computed_branches  *) {result = [];to_avoid = avoid}
     | br::brl' ->
-	(* alpha convertion to prevent name clashes *)
+	(* alpha conversion to prevent name clashes *)
 	let _,idl,patl,return = alpha_br avoid br in
-	let new_avoid  = idl@avoid in 	(* for now we can no more use idl as an indentifier *)
+	let new_avoid  = idl@avoid in 	(* for now we can no more use idl as an identifier *)
 	(* building a list of precondition stating that we are not in this branch
 	   (will be used in the following recursive calls)
 	*)
@@ -1149,7 +1149,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
     | _ -> mkGApp(mkGVar  relname,args@[rt]),Id.Set.empty
 
 
-(* debuging wrapper *)
+(* debugging wrapper *)
 let rebuild_cons env nb_args relname args crossed_types rt =
 (*   observennl  (str "rebuild_cons : rt := "++ pr_glob_constr rt ++  *)
 (* 		 str "nb_args := " ++ str (string_of_int nb_args)); *)
@@ -1163,7 +1163,7 @@ let rebuild_cons env nb_args relname args crossed_types rt =
 (* naive implementation of parameter detection.
 
    A parameter is an argument which is only preceded by parameters and whose
-   calls are all syntaxically equal.
+   calls are all syntactically equal.
 
    TODO: Find a valid way to deal with implicit arguments here!
 *)
@@ -1178,7 +1178,7 @@ let rec compute_cst_params relnames params = function
       compute_cst_params relnames t_params b
   | GCases _ ->
       params  (* If there is still cases at this point they can only be
-		 discriminitation ones *)
+		 discrimination ones *)
   | GSort _ -> params
   | GHole _ -> params
   | GIf _ | GRec _ | GCast _ ->
@@ -1272,7 +1272,7 @@ let do_build_inductive
   in
   let resa = Array.map (build_entry_lc env  funnames_as_set []) rta in
   let env_with_graphs =
-    let rel_arity i funargs =  (* Reduilding arities (with parameters) *)
+    let rel_arity i funargs =  (* Rebuilding arities (with parameters) *)
       let rel_first_args :(Name.t * Glob_term.glob_constr * bool ) list  =
 	funargs
       in
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index b9d7e0d909..0ee8877082 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -45,7 +45,7 @@ let pr_with_bindings prc prlc (c,bl) =
 let pr_constr_with_binding prc (c,bl) :  Pp.std_ppcmds =
   pr_with_bindings prc prc  (c,bl)
 
-(* The local debuging mechanism *)
+(* The local debugging mechanism *)
 (* let msgnl = Pp.msgnl *)
 
 let observe strm =
@@ -255,12 +255,12 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
     let f_principle,princ_type = schemes.(i) in
     let princ_type =  nf_zeta princ_type in
     let princ_infos = Tactics.compute_elim_sig princ_type in
-    (* The number of args of the function is then easilly computable *)
+    (* The number of args of the function is then easily computable *)
     let nb_fun_args = nb_prod (pf_concl g)  - 2  in
     let args_names = generate_fresh_id (Id.of_string "x") [] nb_fun_args in
     let ids = args_names@(pf_ids_of_hyps g) in
-    (* Since we cannot ensure that the funcitonnal principle is defined in the
-       environement and due to the bug #1174, we will need to pose the principle
+    (* Since we cannot ensure that the functional principle is defined in the
+       environment and due to the bug #1174, we will need to pose the principle
        using a name
     *)
     let principle_id = Namegen.next_ident_away_in_goal (Id.of_string "princ") ids in
@@ -522,12 +522,12 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
     let f_principle,princ_type = schemes.(i) in
     let princ_type =  nf_zeta princ_type in
     let princ_infos = Tactics.compute_elim_sig princ_type in
-    (* The number of args of the function is then easilly computable *)
+    (* The number of args of the function is then easily computable *)
     let nb_fun_args = nb_prod (pf_concl g)  - 2  in
     let args_names = generate_fresh_id (Id.of_string "x") [] nb_fun_args in
     let ids = args_names@(pf_ids_of_hyps g) in
-    (* Since we cannot ensure that the funcitonnal principle is defined in the
-       environement and due to the bug #1174, we will need to pose the principle
+    (* Since we cannot ensure that the functional principle is defined in the
+       environment and due to the bug #1174, we will need to pose the principle
        using a name
     *)
     let principle_id = Namegen.next_ident_away_in_goal (Id.of_string "princ") ids in
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index e3dba232b2..0cadffa4fe 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -82,7 +82,7 @@ let search_guard loc env possible_indexes fixdefs =
        iraise (e, info));
     indexes
   else
-    (* we now search recursively amoungst all combinations *)
+    (* we now search recursively among all combinations *)
     (try
        List.iter
 	 (fun l ->
@@ -220,7 +220,7 @@ let process_inference_flags flags env initial_sigma (sigma,c) =
   let c = if flags.expand_evars then nf_evar sigma c else c in
   sigma,c
 
-(* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *)
+(* Allow references to syntactically nonexistent variables (i.e., if applied on an inductive) *)
 let allow_anonymous_refs = ref false
 
 (* Utilisé pour inférer le prédicat des Cases *)
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 7d1e0c9b5b..142b54513e 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -63,7 +63,7 @@ val all_no_fail_flags : inference_flags
 
 val all_and_fail_flags : inference_flags
 
-(** Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *)
+(** Allow references to syntactically nonexistent variables (i.e., if applied on an inductive) *)
 val allow_anonymous_refs : bool ref
   
 (** Generic call to the interpreter from glob_constr to open_constr, leaving
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 203b1ec8a6..01e1154e58 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -673,6 +673,10 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
               (sigma,(k,lift (-nb) cM,fst (extract_instance_status pb))::metasubst,
               evarsubst)
 	    else error_cannot_unify_local curenv sigma (m,n,cM)
+	| Evar (evk,_ as ev), Evar (evk',_)
+            when not (Evar.Set.mem evk flags.frozen_evars)
+              && Evar.equal evk evk' ->
+	    sigma,metasubst,((curenv,ev,cN)::evarsubst)
 	| Evar (evk,_ as ev), _
             when not (Evar.Set.mem evk flags.frozen_evars) 
 	      && not (occur_evar evk cN) ->
@@ -1673,11 +1677,13 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) =
 		 matchrec t
 	       with ex when precatchable_exception ex ->
 		 matchrec c)
+
           | Lambda (_,t,c) ->
 	      (try
 		 matchrec t
 	       with ex when precatchable_exception ex ->
 		 matchrec c)
+
           | _ -> error "Match_subterm"))
   in
   try matchrec cl
@@ -1774,7 +1780,12 @@ let w_unify_to_subterm_list env evd flags hdmeta oplist t =
           try
 	    (* This is up to delta for subterms w/o metas ... *)
 	    w_unify_to_subterm env evd ~flags (strip_outer_cast op,t)
-	  with PretypeError (env,_,NoOccurrenceFound _) when allow_K -> (evd,op)
+	  with PretypeError (env,_,NoOccurrenceFound _) when
+              allow_K ||
+                (* w_unify_to_subterm does not go through evars, so
+                   the next step, which was already in <= 8.4, is
+                   needed at least for compatibility of rewrite *)
+                dependent op t -> (evd,op)
         in
 	  if not allow_K &&
             (* ensure we found a different instance *)
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 4ae64ae65f..2b85ec8724 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -134,7 +134,7 @@ exception FullyUnfocused
 exception CannotUnfocusThisWay
 
 (* This is raised when trying to focus on non-existing subgoals. It is
-   handled by an error message but one may need to catched it and
+   handled by an error message but one may need to catch it and
    settle a better error message in some case (suggesting a better
    bullet for example), see proof_global.ml function Bullet.pop and
    Bullet.push. *)
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index a25683bfcf..b6861fd499 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -192,8 +192,8 @@ let unfocus c sp =
     succeed).  Another benefit is that it is possible to write tactics
     that can be executed even if there are no focused goals.
     - Tactics form a monad ['a tactic], in a sense a tactic can be
-    seens as a function (without argument) which returns a value of
-    type 'a and modifies the environement (in our case: the view).
+    seen as a function (without argument) which returns a value of
+    type 'a and modifies the environment (in our case: the view).
     Tactics of course have arguments, but these are given at the
     meta-level as OCaml functions.  Most tactics in the sense we are
     used to return [()], that is no really interesting values. But
@@ -1126,7 +1126,7 @@ module V82 = struct
     
 
   (* Returns the open goals of the proofview together with the evar_map to 
-     interprete them. *)
+     interpret them. *)
   let goals { comb = comb ; solution = solution; } =
    { Evd.it = comb ; sigma = solution }
 
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index ec255f6a1a..5a9e7f39f0 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -37,7 +37,7 @@ type entry
 val compact : entry -> proofview -> entry * proofview
 
 (** Initialises a proofview, the main argument is a list of
-    environements (including a [named_context] which are used as
+    environments (including a [named_context] which are used as
     hypotheses) pair with conclusion types, creating accordingly many
     initial goals. Because a proof does not necessarily starts in an
     empty [evar_map] (indeed a proof can be triggered by an incomplete
@@ -114,8 +114,8 @@ val unfocus : focus_context -> proofview -> proofview
     succeed).  Another benefit is that it is possible to write tactics
     that can be executed even if there are no focused goals.
     - Tactics form a monad ['a tactic], in a sense a tactic can be
-    seens as a function (without argument) which returns a value of
-    type 'a and modifies the environement (in our case: the view).
+    seen as a function (without argument) which returns a value of
+    type 'a and modifies the environment (in our case: the view).
     Tactics of course have arguments, but these are given at the
     meta-level as OCaml functions.  Most tactics in the sense we are
     used to return [()], that is no really interesting values. But
@@ -230,7 +230,7 @@ val tclBREAK : (iexn -> iexn option) -> 'a tactic -> 'a tactic
     [i] to [j] (see {!focus}). The rest of the goals is restored after
     the tactic action. If the specified range doesn't correspond to
     existing goals, fails with [NoSuchGoals] (a user error). this
-    exception is catched at toplevel with a default message + a hook
+    exception is caught at toplevel with a default message + a hook
     message that can be customized by [set_nosuchgoals_hook] below.
     This hook is used to add a suggestion about bullets when
     applicable. *)
@@ -547,7 +547,7 @@ module V82 : sig
   val grab : proofview -> proofview
 
   (* Returns the open goals of the proofview together with the evar_map to 
-     interprete them. *)
+     interpret them. *)
   val goals : proofview -> Evar.t list Evd.sigma
 
   val top_goals : entry -> proofview -> Evar.t list Evd.sigma
diff --git a/tactics/dnet.ml b/tactics/dnet.ml
index 61a3586627..bb71620c09 100644
--- a/tactics/dnet.ml
+++ b/tactics/dnet.ml
@@ -121,7 +121,7 @@ struct
 	     Idset.union acc s2
 	 ) t Idset.empty)
 
-(*   (\* optimization hack: Not_found is catched in fold_pattern *\) *)
+(*   (\* optimization hack: Not_found is caught in fold_pattern *\) *)
 (*   let fast_inter s1 s2 = *)
 (*     if Idset.is_empty s1 || Idset.is_empty s2 then raise Not_found *)
 (*     else Idset.inter s1 s2 *)
@@ -176,7 +176,7 @@ struct
     let is_empty : t -> bool = function 
       | None -> false
       | Some s -> S.is_empty s
-    (* optimization hack: Not_found is catched in fold_pattern *)
+    (* optimization hack: Not_found is caught in fold_pattern *)
     let fast_inter s1 s2 =
       if is_empty s1 || is_empty s2 then raise Not_found
       else let r = inter s1 s2 in 
diff --git a/test-suite/bugs/closed/2406.v b/test-suite/bugs/closed/2406.v
index 1bd66ffccb..3766e795a0 100644
--- a/test-suite/bugs/closed/2406.v
+++ b/test-suite/bugs/closed/2406.v
@@ -1,6 +1,6 @@
 (* Check correct handling of unsupported notations *)
 Notation "'’'" := (fun x => x) (at level 20).
 
-(* This fails with a syntax error but it is not catched by Fail
+(* This fails with a syntax error but it is not caught by Fail
 Fail Definition crash_the_rooster f := ’.
 *)
diff --git a/test-suite/bugs/closed/2830.v b/test-suite/bugs/closed/2830.v
index b72c821dfd..bb607b785b 100644
--- a/test-suite/bugs/closed/2830.v
+++ b/test-suite/bugs/closed/2830.v
@@ -123,6 +123,7 @@ Module C.
 
 Reserved Notation "a ~> b" (at level 70, right associativity).
 Reserved Notation "a ≈ b" (at level 54).
+Reserved Notation "a ∘ b" (at level 50, left associativity).
 Generalizable All Variables.
 
 Class Category (Object:Type) (Hom:Object -> Object -> Type) := {
diff --git a/test-suite/bugs/closed/3071.v b/test-suite/bugs/closed/3071.v
index 611ac60655..53c2ef7b71 100644
--- a/test-suite/bugs/closed/3071.v
+++ b/test-suite/bugs/closed/3071.v
@@ -2,4 +2,4 @@ Definition foo := True.
 
 Section foo.
   Global Arguments foo / .
-Fail End foo.
+End foo.
diff --git a/test-suite/bugs/closed/3953.v b/test-suite/bugs/closed/3953.v
new file mode 100644
index 0000000000..167cecea8e
--- /dev/null
+++ b/test-suite/bugs/closed/3953.v
@@ -0,0 +1,5 @@
+(* Checking subst on instances of evars (was bugged in 8.5 beta 1) *)
+Goal forall (a b : unit), a = b -> exists c, b = c.
+  intros.
+  eexists.
+  subst.
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index 21b829aa19..a4ed76c5a0 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -536,3 +536,13 @@ Goal forall f:nat->nat, (forall P x, P (f x)) -> let x:=f 0 in x = 0.
 intros f H x.
 apply H.
 Qed.
+
+(* Test that occur-check is not too restrictive (see comments of #3141) *)
+Lemma bar (X: nat -> nat -> Prop) (foo:forall x, X x x) (a: unit) (H: tt = a):
+  exists x, exists y, X x y.
+Proof.
+intros; eexists; eexists; case H.
+apply (foo ?y).
+Grab Existential Variables.
+exact 0.
+Qed.
diff --git a/test-suite/success/rewrite.v b/test-suite/success/rewrite.v
index 6dcd6592b5..62249666b3 100644
--- a/test-suite/success/rewrite.v
+++ b/test-suite/success/rewrite.v
@@ -148,3 +148,13 @@ eexists. intro H.
 rewrite H.
 reflexivity.
 Abort.
+
+(* Check that rewriting within evars still work (was broken in 8.5beta1) *)
+
+
+Goal forall (a: unit) (H: a = tt), exists x y:nat, x = y.
+intros; eexists; eexists.
+rewrite H.
+Undo.
+subst.
+Abort.
diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v
index e39128cb81..65fe87801a 100644
--- a/theories/Program/Utils.v
+++ b/theories/Program/Utils.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** Various syntaxic shortands that are useful with [Program]. *)
+(** Various syntactic shorthands that are useful with [Program]. *)
 
 Require Export Coq.Program.Tactics.