Imported Upstream version 8.5~beta2+dfsgupstream/8.5_beta2+dfsg

14 files changed, 139 insertions, 46 deletions

diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index 9b671bcf..eb108170 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -10,7 +10,6 @@ open Names
 open Term
 open Environ
 open Evd
-open Mod_subst
 open Unification
 open Misctypes
 
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index da40427c..ea204361 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.mli
@@ -8,7 +8,6 @@
 
 open Term
 open Clenv
-open Proof_type
 open Tacexpr
 open Unification
 
diff --git a/proofs/goal.ml b/proofs/goal.ml
index e3570242..107ce7f8 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -9,8 +9,6 @@
 open Util
 open Pp
 open Term
-open Vars
-open Context
 
 (* This module implements the abstract interface to goals *)
 (* A general invariant of the module, is that a goal whose associated
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 53f8093e..b8206ca1 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -13,7 +13,6 @@ open Names
 open Nameops
 open Term
 open Vars
-open Context
 open Termops
 open Environ
 open Reductionops
@@ -83,12 +82,6 @@ let apply_to_hyp sign id f =
     if !check then error_no_such_hypothesis id
     else sign
 
-let apply_to_hyp_and_dependent_on sign id f g =
-  try apply_to_hyp_and_dependent_on sign id f g
-  with Hyp_not_found ->
-    if !check then error_no_such_hypothesis id
-    else sign
-
 let check_typability env sigma c =
   if !check then let _ = type_of env sigma c in ()
 
@@ -277,11 +270,6 @@ let move_hyp toleft (left,(idfrom,_,_ as declfrom),right) hto =
     List.fold_left (fun sign d -> push_named_context_val d sign)
       right left
 
-let rename_hyp id1 id2 sign =
-  apply_to_hyp_and_dependent_on sign id1
-    (fun (_,b,t) _ -> (id2,b,t))
-    (fun d _ -> map_named_declaration (replace_vars [id1,mkVar id2]) d)
-
 (**********************************************************************)
 
 
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index fdc93bcb..d1b6afe2 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -156,6 +156,41 @@ let build_by_tactic env ctx ?(poly=false) typ tac =
   assert(Univ.ContextSet.is_empty ctx);
   cb, status, univs
 
+let refine_by_tactic env sigma ty tac =
+  (** Save the initial side-effects to restore them afterwards. We set the
+      current set of side-effects to be empty so that we can retrieve the
+      ones created during the tactic invocation easily. *)
+  let eff = Evd.eval_side_effects sigma in
+  let sigma = Evd.drop_side_effects sigma in
+  (** Start a proof *)
+  let prf = Proof.start sigma [env, ty] in
+  let (prf, _) =
+    try Proof.run_tactic env tac prf
+    with Logic_monad.TacticFailure e as src ->
+      (** Catch the inner error of the monad tactic *)
+      let (_, info) = Errors.push src in
+      iraise (e, info)
+  in
+  (** Plug back the retrieved sigma *)
+  let sigma = Proof.in_proof prf (fun sigma -> sigma) in
+  let ans = match Proof.initial_goals prf with
+  | [c, _] -> c
+  | _ -> assert false
+  in
+  let ans = Reductionops.nf_evar sigma ans in
+  (** [neff] contains the freshly generated side-effects *)
+  let neff = Evd.eval_side_effects sigma in
+  (** Reset the old side-effects *)
+  let sigma = Evd.drop_side_effects sigma in
+  let sigma = Evd.emit_side_effects eff sigma in
+  (** Get rid of the fresh side-effects by internalizing them in the term
+      itself. Note that this is unsound, because the tactic may have solved
+      other goals that were already present during its invocation, so that
+      those goals rely on effects that are not present anymore. Hopefully,
+      this hack will work in most cases. *)
+  let ans = Term_typing.handle_side_effects env ans neff in
+  ans, sigma
+
 (**********************************************************************)
 (* Support for resolution of evars in tactic interpretation, including
    resolution by application of tactics *)
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index edbc18a3..5e0fb4dd 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -157,6 +157,14 @@ val build_by_tactic : env -> Evd.evar_universe_context -> ?poly:polymorphic ->
   types -> unit Proofview.tactic -> 
   constr * bool * Evd.evar_universe_context
 
+val refine_by_tactic : env -> Evd.evar_map -> types -> unit Proofview.tactic ->
+  constr * Evd.evar_map
+(** A variant of the above function that handles open terms as well.
+    Caveat: all effects are purged in the returned term at the end, but other
+    evars solved by side-effects are NOT purged, so that unexpected failures may
+    occur. Ideally all code using this function should be rewritten in the
+    monad. *)
+
 (** Declare the default tactic to fill implicit arguments *)
 
 val declare_implicit_tactic : unit Proofview.tactic -> unit
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 4ae64ae6..2b85ec87 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/proof_global.ml b/proofs/proof_global.ml
index f55ab700..5bff3c81 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -74,7 +74,7 @@ type proof_object = {
 }
 
 type proof_ending =
-  | Admitted
+  | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry
   | Proved of Vernacexpr.opacity_flag *
              (Vernacexpr.lident * Decl_kinds.theorem_kind option) option *
               proof_object
@@ -295,7 +295,7 @@ let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl =
 	let ctx = Evd.evar_universe_context_set universes in
         if keep_body_ucst_sepatate then
           (* For vi2vo compilation proofs are computed now but we need to
-           * completent the univ constraints of the typ with the ones of
+           * complement the univ constraints of the typ with the ones of
            * the body.  So we keep the two sets distinct. *)
           let ctx_body = restrict_universe_context ctx used_univs_body in
           let ctx_typ = restrict_universe_context ctx used_univs_typ in
@@ -338,21 +338,37 @@ let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl =
 
 type closed_proof_output = (Term.constr * Declareops.side_effects) list * Evd.evar_universe_context
 
-let return_proof () =
-  let { proof; strength = (_,poly,_) } = cur_pstate () in
+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
+    msg_warning (str"The proof of " ++ str (Names.Id.to_string pid) ++
+     str" is complete, no need to end it with Admitted");
+  end;
+  let proofs = Proof.partial_proof proof in
+  let _,_,_,_, evd = Proof.proof proof in
+  let eff = Evd.eval_side_effects evd in
+  (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
+      side-effects... This may explain why one need to uniquize side-effects
+      thereafter... *)
+  let proofs = List.map (fun c -> c, eff) proofs in
+    proofs, Evd.evar_universe_context evd
+ end else
   let initial_goals = Proof.initial_goals proof in
   let evd =
-    let error s = raise (Errors.UserError("last tactic before Qed",s)) in
+    let error s =
+      let prf = str " (in proof " ++ Id.print pid ++ str ")" in
+      raise (Errors.UserError("last tactic before Qed",s ++ prf))
+    in
     try Proof.return proof with
     | Proof.UnfinishedProof ->
         error(str"Attempt to save an incomplete proof")
     | Proof.HasShelvedGoals ->
         error(str"Attempt to save a proof with shelved goals")
     | Proof.HasGivenUpGoals ->
-        error(str"Attempt to save a proof with given up goals")
+        error(strbrk"Attempt to save a proof with given up goals. If this is really what you want to do, use Admitted in place of Qed.")
     | Proof.HasUnresolvedEvar->
-        error(str"Attempt to save a proof with existential " ++
-              str"variables still non-instantiated") in
+        error(strbrk"Attempt to save a proof with existential variables still non-instantiated") in
   let eff = Evd.eval_side_effects evd in
   let evd =
     if poly || !Flags.compilation_mode = Flags.BuildVo
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 2700e901..9d5038a3 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -66,7 +66,7 @@ type proof_object = {
 }
 
 type proof_ending =
-  | Admitted
+  | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry
   | Proved of Vernacexpr.opacity_flag *
              (Vernacexpr.lident * Decl_kinds.theorem_kind option) option *
               proof_object
@@ -99,7 +99,9 @@ val close_proof : keep_body_ucst_sepatate:bool -> Future.fix_exn -> closed_proof
 
 type closed_proof_output = (Term.constr * Declareops.side_effects) list * Evd.evar_universe_context
 
-val return_proof : unit -> closed_proof_output
+(* If allow_partial is set (default no) then an incomplete proof
+ * is allowed (no error), and a warn is given if the proof is complete. *)
+val return_proof : ?allow_partial:bool -> unit -> closed_proof_output
 val close_future_proof : feedback_id:Stateid.t ->
   closed_proof_output Future.computation -> closed_proof
 
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 26bb78df..47b2b255 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -10,7 +10,6 @@
 open Evd
 open Names
 open Term
-open Context
 open Tacexpr
 open Glob_term
 open Nametab
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index e709be5b..f5e2bad2 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -9,7 +9,6 @@
 open Evd
 open Names
 open Term
-open Context
 open Tacexpr
 open Glob_term
 open Nametab
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index a25683bf..6f626341 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
@@ -719,22 +719,72 @@ let give_up =
 
 (** {7 Control primitives} *)
 
-(** Equality function on goals *)
-let goal_equal evars1 gl1 evars2 gl2 =
-  let evi1 = Evd.find evars1 gl1 in
-  let evi2 = Evd.find evars2 gl2 in
-  Evd.eq_evar_info evars2 evi1 evi2
+
+module Progress = struct
+
+  (** equality function up to evar instantiation in heterogeneous
+      contexts. *)
+  (* spiwack (2015-02-19): In the previous version of progress an
+     equality which considers two universes equal when it is consistent
+     tu unify them ([Evd.eq_constr_univs_test]) was used. Maybe this
+     behaviour has to be restored as well. This has to be established by
+     practice. *)
+    
+  let rec eq_constr sigma1 sigma2 t1 t2 =
+    Constr.equal_with
+      (fun t -> Evarutil.kind_of_term_upto sigma1 t)
+      (fun t -> Evarutil.kind_of_term_upto sigma2 t)
+      t1 t2
+
+  (** equality function on hypothesis contexts *)
+  let eq_named_context_val sigma1 sigma2 ctx1 ctx2 =
+    let open Environ in
+    let c1 = named_context_of_val ctx1 and c2 = named_context_of_val ctx2 in
+    let eq_named_declaration (i1, c1, t1) (i2, c2, t2) =
+      Names.Id.equal i1 i2 && Option.equal (eq_constr sigma1 sigma2) c1 c2 
+      && (eq_constr sigma1 sigma2) t1 t2
+    in List.equal eq_named_declaration c1 c2
+
+  let eq_evar_body sigma1 sigma2 b1 b2 =
+    let open Evd in
+    match b1, b2 with
+    | Evar_empty, Evar_empty -> true
+    | Evar_defined t1, Evar_defined t2 -> eq_constr sigma1 sigma2 t1 t2
+    | _ -> false
+
+  let eq_evar_info sigma1 sigma2 ei1 ei2 =
+    let open Evd in
+    eq_constr sigma1 sigma2 ei1.evar_concl ei2.evar_concl &&
+    eq_named_context_val sigma1 sigma2 (ei1.evar_hyps) (ei2.evar_hyps) &&
+    eq_evar_body sigma1 sigma2 ei1.evar_body ei2.evar_body
+
+  (** Equality function on goals *)
+  let goal_equal evars1 gl1 evars2 gl2 =
+    let evi1 = Evd.find evars1 gl1 in
+    let evi2 = Evd.find evars2 gl2 in
+    eq_evar_info evars1 evars2 evi1 evi2
+
+end
 
 let tclPROGRESS t =
   let open Proof in
   Pv.get >>= fun initial ->
   t >>= fun res ->
   Pv.get >>= fun final ->
+  (* [*_test] test absence of progress. [quick_test] is approximate
+     whereas [exhaustive_test] is complete. *)
+  let quick_test =
+    initial.solution == final.solution && initial.comb == final.comb
+  in
+  let exhaustive_test =
+    Util.List.for_all2eq begin fun i f ->
+      Progress.goal_equal initial.solution i final.solution f
+    end initial.comb final.comb
+  in
   let test =
-    Evd.progress_evar_map initial.solution final.solution &&
-    not (Util.List.for_all2eq (fun i f -> goal_equal initial.solution i final.solution f) initial.comb final.comb)
+    quick_test || exhaustive_test
   in
-  if test then
+  if not test then
     tclUNIT res
   else
     tclZERO (Errors.UserError ("Proofview.tclPROGRESS" , Pp.str"Failed to progress."))
@@ -1126,7 +1176,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 ec255f6a..5a9e7f39 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/proofs/redexpr.ml b/proofs/redexpr.ml
index 18588867..1383d755 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -234,7 +234,7 @@ let reduction_of_red_expr env =
 	 with Not_found ->
 	   error("unknown user-defined reduction \""^s^"\"")))
   | CbvVm o -> (contextualize cbv_vm cbv_vm o, VMcast)
-  | CbvNative o -> (contextualize cbv_native cbv_native o, VMcast)
+  | CbvNative o -> (contextualize cbv_native cbv_native o, NATIVEcast)
   in
     reduction_of_red_expr