Merge branch 'master'.

7 files changed, 62 insertions, 12 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index b6b202cd9..f50a8b850 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -634,6 +634,9 @@ let closedn sigma n c =
 
 let closed0 sigma c = closedn sigma 0 c
 
+let subst_of_rel_context_instance ctx subst =
+  List.map of_constr (Vars.subst_of_rel_context_instance (List.map unsafe_to_rel_decl ctx) (List.map to_constr subst))
+
 end
 
 let rec isArity sigma c =
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 3b479a64d..1ae71216f 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -195,6 +195,8 @@ val closedn : Evd.evar_map -> int -> t -> bool
 val closed0 : Evd.evar_map -> t -> bool
 
 val subst_univs_level_constr : Univ.universe_level_subst -> t -> t
+val subst_of_rel_context_instance : rel_context -> t list -> t list
+
 
 end
 
diff --git a/engine/evd.ml b/engine/evd.ml
index b8f4b126a..0ea15dd21 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -664,13 +664,16 @@ let restrict evk filter ?candidates evd =
     { evar_info with evar_filter = filter;
       evar_candidates = candidates;
       evar_extra = Store.empty } in
+  let last_mods = match evd.conv_pbs with
+  | [] ->  evd.last_mods
+  | _ -> Evar.Set.add evk evd.last_mods in
   let evar_names = EvNames.reassign_name_defined evk evk' evd.evar_names in
   let ctxt = Filter.filter_list filter (evar_context evar_info) in
   let id_inst = Array.map_of_list (NamedDecl.get_id %> mkVar) ctxt in
   let body = mkEvar(evk',id_inst) in
   let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
   { evd with undf_evars = EvMap.add evk' evar_info' undf_evars;
-    defn_evars; evar_names }, evk'
+    defn_evars; last_mods; evar_names }, evk'
 
 let downcast evk ccl evd =
   let evar_info = EvMap.find evk evd.undf_evars in
@@ -829,6 +832,13 @@ let is_eq_sort s1 s2 =
       if Univ.Universe.equal u1 u2 then None
       else Some (u1, u2)
 
+(* Precondition: l is not defined in the substitution *)
+let universe_rigidity evd l =
+  let uctx = evd.universes in
+  if Univ.LSet.mem l (Univ.ContextSet.levels (UState.context_set uctx)) then
+    UnivFlexible (Univ.LSet.mem l (UState.algebraics uctx))
+  else UnivRigid
+
 let normalize_universe evd =
   let vars = ref (UState.subst evd.universes) in
   let normalize = Universes.normalize_universe_opt_subst vars in
diff --git a/engine/evd.mli b/engine/evd.mli
index 2151000b6..9c6cd60bc 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -463,7 +463,17 @@ val retract_coercible_metas : evar_map -> metabinding list * evar_map
 (*********************************************************
    Sort/universe variables *)
 
-(** Rigid or flexible universe variables *)
+(** Rigid or flexible universe variables.
+
+   [UnivRigid] variables are user-provided or come from an explicit
+   [Type] in the source, we do not minimize them or unify them eagerly.
+
+   [UnivFlexible alg] variables are fresh universe variables of
+   polymorphic constants or generated during refinement, sometimes in
+   algebraic position (i.e. not appearing in the term at the moment of
+   creation). They are the candidates for minimization (if alg, to an
+   algebraic universe) and unified eagerly in the first-order
+   unification heurstic.  *)
 
 type rigid = UState.rigid =
   | UnivRigid
@@ -510,7 +520,8 @@ val new_univ_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_
 val new_sort_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * sorts
 
 val add_global_univ : evar_map -> Univ.Level.t -> evar_map
-											   
+
+val universe_rigidity : evar_map -> Univ.Level.t -> rigid
 val make_flexible_variable : evar_map -> bool -> Univ.universe_level -> evar_map
 val is_sort_variable : evar_map -> sorts -> Univ.universe_level option 
 (** [is_sort_variable evm s] returns [Some u] or [None] if [s] is 
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 71e9acc88..9c264439b 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -424,11 +424,11 @@ let tclFOCUSID id t =
 
 exception SizeMismatch of int*int
 let _ = CErrors.register_handler begin function
-  | SizeMismatch (i,_) ->
+  | SizeMismatch (i,j) ->
       let open Pp in
       let errmsg =
         str"Incorrect number of goals" ++ spc() ++
-        str"(expected "++int i++str(String.plural i " tactic") ++ str")."
+        str"(expected "++int i++str(String.plural i " tactic") ++ str", was given "++ int j++str")."
       in
       CErrors.user_err  errmsg
   | _ -> raise CErrors.Unhandled
@@ -454,6 +454,25 @@ let iter_goal i =
   Solution.get >>= fun evd ->
   Comb.set CList.(undefined evd (flatten (rev subgoals)))
 
+(** List iter but allocates a list of results *)
+let map_goal i =
+  let rev = List.rev in (* hem... Proof masks List... *)
+  let open Proof in
+  Comb.get >>= fun initial ->
+  Proof.List.fold_left begin fun (acc, subgoals as cur) goal ->
+    Solution.get >>= fun step ->
+    match Evarutil.advance step goal with
+    | None -> return cur
+    | Some goal ->
+        Comb.set [goal] >>
+        i goal >>= fun res ->
+        Proof.map (fun comb -> comb :: subgoals) Comb.get >>= fun x ->
+        return (res :: acc, x)
+  end ([],[]) initial >>= fun (results_rev, subgoals) ->
+  Solution.get >>= fun evd ->
+  Comb.set CList.(undefined evd (flatten (rev subgoals))) >>
+  return (rev results_rev)
+
 (** A variant of [Monad.List.fold_left2] where the first list is the
     list of focused goals. The argument tactic is executed in a focus
     comprising only of the current goal, a goal which has been solved
@@ -586,7 +605,15 @@ let tclINDEPENDENT tac =
       let tac = InfoL.tag (Info.DBranch) tac in
       InfoL.tag (Info.Dispatch) (iter_goal (fun _ -> tac))
 
-
+let tclINDEPENDENTL tac =
+  let open Proof in
+  Pv.get >>= fun initial ->
+  match initial.comb with
+  | [] -> tclUNIT []
+  | [_] -> tac >>= fun x -> return [x]
+  | _ ->
+      let tac = InfoL.tag (Info.DBranch) tac in
+      InfoL.tag (Info.Dispatch) (map_goal (fun _ -> tac))
 
 (** {7 Goal manipulation} *)
 
@@ -1157,10 +1184,6 @@ let tclLIFT = Proof.lift
 let tclCHECKINTERRUPT =
    tclLIFT (NonLogical.make Control.check_for_interrupt)
 
-
-
-
-
 (*** Compatibility layer with <= 8.2 tactics ***)
 module V82 = struct
   type tac = Evar.t Evd.sigma -> Evar.t list Evd.sigma
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 4f662b294..a3b0304b1 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -293,6 +293,7 @@ val tclEXTEND : unit tactic list -> unit tactic -> unit tactic list -> unit tact
     independent of backtracking in another. It is equivalent to
     [tclEXTEND [] tac []]. *)
 val tclINDEPENDENT : unit tactic -> unit tactic
+val tclINDEPENDENTL: 'a tactic -> 'a list tactic
 
 
 (** {7 Goal manipulation} *)
@@ -374,7 +375,6 @@ val mark_as_unsafe : unit tactic
     with given up goals cannot be closed. *)
 val give_up : unit tactic
 
-
 (** {7 Control primitives} *)
 
 (** [tclPROGRESS t] checks the state of the proof after [t]. It it is
diff --git a/engine/termops.ml b/engine/termops.ml
index d8e712abc..410fb75c5 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -185,6 +185,7 @@ let pr_decl (decl,ok) =
                            print_constr c ++ str (if ok then ")" else "}")
 
 let pr_evar_source = function
+  | Evar_kinds.NamedHole id -> pr_id id
   | Evar_kinds.QuestionMark _ -> str "underscore"
   | Evar_kinds.CasesType false -> str "pattern-matching return predicate"
   | Evar_kinds.CasesType true ->
@@ -1368,7 +1369,7 @@ let smash_rel_context sign =
 let fold_named_context_both_sides f l ~init = List.fold_right_and_left f l init
 
 let mem_named_context_val id ctxt =
-  try Environ.lookup_named_val id ctxt; true with Not_found -> false
+  try ignore(Environ.lookup_named_val id ctxt); true with Not_found -> false
 
 let map_rel_decl f = function
 | RelDecl.LocalAssum (id, t) -> RelDecl.LocalAssum (id, f t)