Porting Tactics.assumption to the new engine.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17073 85f007b7-540e-0410-9357-904b9bb8a0f7

8 files changed, 41 insertions, 24 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 1205d97001..e87158bdde 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -1270,7 +1270,7 @@ let exists_evaluable_reference env = function
   | EvalVarRef v -> try ignore(lookup_named v env); true with Not_found -> false
 
 let dbg_intro dbg = new_tclLOG dbg (fun () -> str "intro") intro
-let dbg_assumption dbg = tclLOG dbg (fun () -> str "assumption") assumption
+let dbg_assumption dbg = new_tclLOG dbg (fun () -> str "assumption") assumption
 
 let rec trivial_fail_db dbg mod_delta db_list local_db =
   let intro_tac =
@@ -1286,7 +1286,7 @@ let rec trivial_fail_db dbg mod_delta db_list local_db =
   Proofview.Goal.enter begin fun gl ->
     let concl = Proofview.Goal.concl gl in
     Tacticals.New.tclFIRST
-      ((Proofview.V82.tactic (dbg_assumption dbg))::intro_tac::
+      ((dbg_assumption dbg)::intro_tac::
           (List.map Tacticals.New.tclCOMPLETE
              (trivial_resolve dbg mod_delta db_list local_db concl)))
   end
@@ -1441,7 +1441,7 @@ let search d n mod_delta db_list local_db =
        each goal. Hence the [tclEXTEND] *)
     Proofview.tclEXTEND [] begin
       if Int.equal n 0 then Proofview.tclZERO (Errors.UserError ("",str"BOUND 2")) else
-        Tacticals.New.tclORELSE0 (Proofview.V82.tactic (dbg_assumption d))
+        Tacticals.New.tclORELSE0 (dbg_assumption d)
 	  (Tacticals.New.tclORELSE0 (intro_register d (search d n) local_db)
 	     ( Proofview.Goal.enter begin fun gl ->
                let concl = Proofview.Goal.concl gl in
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 19e5906f85..0198fc3fdf 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -91,7 +91,7 @@ let contradiction_term (c,lbind as cl) =
       let typ = type_of c in
       let _, ccl = splay_prod env sigma typ in
       if is_empty_type ccl then
-        Tacticals.New.tclTHEN (elim false cl None) (Proofview.V82.tactic (tclTRY assumption))
+        Tacticals.New.tclTHEN (elim false cl None) (Tacticals.New.tclTRY assumption)
       else
         Proofview.tclORELSE
           begin
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 36cb55e5b4..7c72d8ad50 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -531,8 +531,8 @@ let multi_replace clause c2 c1 unsafe try_prove_eq_opt =
 	  (Tacticals.New.tclTRY (general_multi_rewrite false false (mkVar id,NoBindings) clause))
 	  (Proofview.V82.tactic (clear [id])));
        Tacticals.New.tclFIRST
-	 [Proofview.V82.tactic assumption;
-	  Tacticals.New.tclTHEN (Proofview.V82.tactic (apply sym)) (Proofview.V82.tactic assumption);
+	 [assumption;
+	  Tacticals.New.tclTHEN (Proofview.V82.tactic (apply sym)) assumption;
 	  try_prove_eq
 	 ]
       ]
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index f816983706..ad76543744 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -29,7 +29,7 @@ val h_intro_move      : Id.t option -> Id.t move_location -> unit Proofview.tact
 val h_intro           : Id.t -> unit Proofview.tactic
 val h_intros_until    : quantified_hypothesis -> unit Proofview.tactic
 
-val h_assumption      : tactic
+val h_assumption      : unit Proofview.tactic
 val h_exact           : constr -> tactic
 val h_exact_no_check  : constr -> tactic
 val h_vm_cast_no_check  : constr -> tactic
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index f40ec76595..337ae52416 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1835,7 +1835,7 @@ let setoid_symmetry_in id =
   let new_hyp = it_mkProd_or_LetIn new_hyp'  binders in
     Tacticals.New.tclTHENS (Proofview.V82.tactic (Tactics.cut new_hyp))
       [ Proofview.V82.tactic (intro_replacing id);
-	Tacticals.New.tclTHENLIST [ intros; setoid_symmetry; Proofview.V82.tactic (apply (mkVar id)); Proofview.V82.tactic (Tactics.assumption) ] ]
+	Tacticals.New.tclTHENLIST [ intros; setoid_symmetry; Proofview.V82.tactic (apply (mkVar id)); Tactics.assumption ] ]
   end
 
 let _ = Hook.set Tactics.setoid_reflexivity setoid_reflexivity
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 34314088c0..248a5d36bf 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1756,7 +1756,7 @@ and interp_atomic ist tac =
         let mloc = Tacmach.New.of_old (fun gl -> interp_move_location ist gl hto) gl in
         h_intro_move (Option.map (interp_fresh_ident ist env) ido) mloc
       end
-  | TacAssumption -> Proofview.V82.tactic h_assumption
+  | TacAssumption -> h_assumption
   | TacExact c ->
       Proofview.V82.tactic begin fun gl -> 
         let (sigma,c_interp) = pf_interp_casted_constr ist gl c in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 0bf295b3cb..2f52c8b7a5 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1166,19 +1166,36 @@ let exact_proof c gl =
   let c = Constrintern.interp_casted_constr (project gl) (pf_env gl) c (pf_concl gl)
   in refine_no_check c gl
 
-let (assumption : tactic) = fun gl ->
-  let concl =  pf_concl gl in
-  let hyps = pf_hyps gl in
-  let rec arec only_eq = function
-    | [] ->
-        if only_eq then arec false hyps else error "No such assumption."
-    | (id,c,t)::rest ->
-	if (only_eq && eq_constr t concl)
-          || (not only_eq && pf_conv_x_leq gl t concl)
-        then refine_no_check (mkVar id) gl
-	else arec only_eq rest
+let tclZEROMSG msg =
+  Proofview.tclZERO (UserError ("", msg))
+
+let assumption =
+  let rec arec gl only_eq = function
+  | [] ->
+    if only_eq then
+      let hyps = Proofview.Goal.hyps gl in
+      arec gl false hyps
+    else tclZEROMSG (str "No such assumption.")
+  | (id, c, t)::rest ->
+    let concl = Proofview.Goal.concl gl in
+    let is_same_type =
+      if only_eq then eq_constr t concl
+      else
+        let sigma = Proofview.Goal.sigma gl in
+        let env = Proofview.Goal.env gl in
+        is_conv_leq env sigma t concl
+    in
+    if is_same_type then
+      let c = Goal.Refinable.make (fun _ -> Goal.return (mkVar id)) in
+      let r = Goal.bind c Goal.refine in
+      Proofview.tclSENSITIVE r
+    else arec gl only_eq rest
+  in
+  let assumption_tac gl =
+    let hyps = Proofview.Goal.hyps gl in
+    arec gl true hyps
   in
-  arec true hyps
+  Proofview.Goal.enter assumption_tac
 
 (*****************************************************************)
 (*          Modification of a local context                      *)
@@ -3688,7 +3705,7 @@ let symmetry_in id =
           | HeterogenousEq (t1,c1,t2,c2) -> mkApp (hdcncl, [| t2; c2; t1; c1 |]) in
         Tacticals.New.tclTHENS (Proofview.V82.tactic (cut (it_mkProd_or_LetIn symccl sign)))
           [ Proofview.V82.tactic (intro_replacing id);
-            Tacticals.New.tclTHENLIST [ intros; symmetry; Proofview.V82.tactic (apply (mkVar id)); Proofview.V82.tactic assumption ] ]
+            Tacticals.New.tclTHENLIST [ intros; symmetry; Proofview.V82.tactic (apply (mkVar id)); assumption ] ]
     end
     begin function
       | NoEquationFound -> Hook.get forward_setoid_symmetry_in id
@@ -3739,7 +3756,7 @@ let prove_transitivity hdcncl eq_kind t =
        (Tacticals.New.tclTHENLIST
 	  [ Tacticals.New.tclDO 2 intro;
 	    Tacticals.New.onLastHyp simplest_case;
-	    Proofview.V82.tactic assumption ]))
+	    assumption ]))
   end
 
 let transitivity_red allowred t =
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index fc4c780fe8..c3df47215a 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -120,7 +120,7 @@ val intros_pattern :
 
 (** {6 Exact tactics. } *)
 
-val assumption       : tactic
+val assumption       : unit Proofview.tactic
 val exact_no_check   : constr -> tactic
 val vm_cast_no_check : constr -> tactic
 val exact_check      : constr -> tactic