Suppression du test de convertibilite inutile pour la plupart des exact; 2 versions exact_no_check, exact_check

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

8 files changed, 36 insertions, 31 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index dd11121526..89f84332ea 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -644,7 +644,7 @@ and my_find_search db_list local_db hdc concl =
 	match t with
 	  | Res_pf (term,cl)  -> unify_resolve (term,cl)
 	  | ERes_pf (_,c) -> (fun gl -> error "eres_pf")
-	  | Give_exact c  -> exact c
+	  | Give_exact c  -> exact_no_check c
 	  | Res_pf_THEN_trivial_fail (term,cl) -> 
 	      tclTHEN 
 		(unify_resolve (term,cl)) 
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 49131d1926..e4b1ac15ad 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -16,7 +16,7 @@ open Pattern
 open Clenv
 open Auto
 
-let e_give_exact c gl = tclTHEN (unify (pf_type_of gl c)) (Tactics.exact c) gl
+let e_give_exact c gl = tclTHEN (unify (pf_type_of gl c)) (exact_no_check c) gl
 
 let assumption id = e_give_exact (mkVar id)
         
diff --git a/tactics/elim.ml b/tactics/elim.ml
index fc0dec451e..b4eaf03e83 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -80,7 +80,7 @@ let general_decompose recognizer c gl =
   (tclTHENS (cut typc) 
      [(tclTHEN (intro_using tmphyp_name)
          (onLastHyp (general_decompose_clause recognizer)));
-      (exact c)]) gl
+      (exact_no_check c)]) gl
 
 let head_in gls indl t =
   try
diff --git a/tactics/equality.ml b/tactics/equality.ml
index b1d0348d3c..09c8767e23 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1046,7 +1046,7 @@ let swapEquandsInConcl gls =
 let swapEquandsInHyp id gls =
   ((tclTHENS (cut_replacing id (swap_equands gls (clause_type (Some id) gls)))
       ([tclIDTAC;
-      	(tclTHEN (swapEquandsInConcl) (exact (mkVar id)))]))) gls
+      	(tclTHEN (swapEquandsInConcl) (exact_no_check (mkVar id)))]))) gls
 
 (* find_elim determines which elimination principle is necessary to
    eliminate lbeq on sort_of_gl. It yields the boolean true wether
@@ -1205,7 +1205,7 @@ let substInHyp eqn id gls =
   (tclTHENS (cut_replacing id (subst1 e2 body))
      ([tclIDTAC;
        (tclTHENS (bareRevSubstInConcl lbeq body (t,e1,e2))
-          ([exact (mkVar id);tclIDTAC]))])) gls
+          ([exact_no_check (mkVar id);tclIDTAC]))])) gls
 
 let revSubstInHyp eqn id gls =
   (tclTHENS (substInHyp (swap_equands gls eqn) id)
@@ -1432,7 +1432,7 @@ let rewrite_in lR com id gls =
     (try 
        (tclTHENS 
           ((if lR then substInHyp else revSubstInHyp) eqn id) 
-          ([tclIDTAC ; exact c])) gls
+          ([tclIDTAC ; exact_no_check c])) gls
      with UserError("SubstInHyp",_) -> tclIDTAC gls)
   with UserError ("find_eq_data_decompose",_)->  
     errorlabstrm "rewrite_in" [< 'sTR"No equality here" >] 
@@ -1469,10 +1469,10 @@ let hypSubst id cls gls =
   match cls with
     | None -> 
 	(tclTHENS (substInConcl (clause_type (Some id) gls))
-	   ([tclIDTAC; exact (mkVar id)])) gls
+	   ([tclIDTAC; exact_no_check (mkVar id)])) gls
     | Some hypid -> 
 	(tclTHENS (substInHyp (clause_type (Some id) gls) hypid)
-	   ([tclIDTAC;exact (mkVar id)])) gls
+	   ([tclIDTAC;exact_no_check (mkVar id)])) gls
 
 (* id:a=b |- (P a)
  * HypSubst id.
@@ -1524,10 +1524,10 @@ let revHypSubst id cls gls =
   match cls with
     | None -> 
 	(tclTHENS (revSubstInConcl (clause_type (Some id) gls))
-	   ([tclIDTAC; exact (mkVar id)])) gls
+	   ([tclIDTAC; exact_no_check (mkVar id)])) gls
     | Some hypid -> 
 	(tclTHENS (revSubstInHyp (clause_type (Some id) gls) hypid)
-	   ([tclIDTAC;exact (mkVar id)])) gls
+	   ([tclIDTAC;exact_no_check (mkVar id)])) gls
 
 (* id:a=b |- (P b)
  * HypSubst id.
diff --git a/tactics/tacentries.ml b/tactics/tacentries.ml
index 4031a11c13..90003dc344 100644
--- a/tactics/tacentries.ml
+++ b/tactics/tacentries.ml
@@ -17,7 +17,7 @@ let v_introsUntil   = hide_tactic "IntrosUntil"   dyn_intros_until
 (*let v_tclIDTAC      = hide_tactic "Idtac"         dyn_tclIDTAC
 let v_tclFAIL       = hide_tactic "Fail"          dyn_tclFAIL*)
 let v_assumption    = hide_tactic "Assumption"    dyn_assumption
-let v_exact         = hide_tactic "Exact"         dyn_exact
+let v_exact         = hide_tactic "Exact"         dyn_exact_check
 let v_reduce        = hide_tactic "Reduce"        dyn_reduce
 let v_change        = hide_tactic "Change"        dyn_change
 let v_constructor   = hide_tactic "Constructor"   dyn_constructor
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 48ddc16ce6..adf147b869 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -729,7 +729,7 @@ let dyn_lettac args gl = match args with
 (*               Exact tactics                                      *)
 (********************************************************************)
 
-let exact c gl =
+let exact_check c gl =
   let concl = (pf_concl gl) in
   let ct = pf_type_of gl c in
   if pf_conv_x_leq gl ct concl then  
@@ -737,21 +737,25 @@ let exact c gl =
   else 
     error "Not an exact proof"
 
-(*
-let dyn_exact =  
-  function [(COMMAND com)] -> tactic_com exact com
-           | l             -> bad_tactic_args "exact" l
- 
-*)
+let exact_no_check = refine
+
+let dyn_exact_no_check cc gl = match cc with
+  | [Constr c] -> exact_no_check c gl
+  | [Command com] ->
+      let evc = (project gl) in
+      let concl = (pf_concl gl) in
+      let c = Astterm.interp_casted_constr evc (pf_env gl) com concl in
+      refine c gl 
+  | l -> bad_tactic_args "exact_no_check" l 
 
-let dyn_exact cc gl = match cc with
-  | [Constr c] -> exact c gl
+let dyn_exact_check cc gl = match cc with
+  | [Constr c] -> exact_check c gl
   | [Command com] ->
       let evc = (project gl) in
       let concl = (pf_concl gl) in
       let c = Astterm.interp_casted_constr evc (pf_env gl) com concl in
       refine c gl 
-  | l -> bad_tactic_args "exact" l 
+  | l -> bad_tactic_args "exact_check" l 
 
 let (assumption : tactic) = fun gl ->
   let concl =  pf_concl gl in 
@@ -822,7 +826,7 @@ let new_hyp mopt c blist g =
   in 
   (tclTHENL (tclTHEN (kONT clause.hook)
                (cut (pf_type_of g cut_pf)))
-     ((tclORELSE (apply cut_pf) (exact cut_pf)))) g
+     ((tclORELSE (apply cut_pf) (exact_no_check cut_pf)))) g
 
 let dyn_new_hyp argsl gl =
   match argsl with 
@@ -1523,7 +1527,7 @@ let absurd c gls =
 	       ((fun gl ->
 		   let ida = pf_nth_hyp_id gl 1
                    and idna = pf_nth_hyp_id gl 2 in
-                   exact (applist(mkVar idna,[mkVar ida])) gl)));
+                   exact_no_check (applist(mkVar idna,[mkVar ida])) gl)));
             tclIDTAC]));
        tclIDTAC])) gls
 
@@ -1667,7 +1671,7 @@ let abstract_subproof name tac gls =
     let newenv = Global.env() in
     Declare.construct_reference newenv CCI na
   in
-  exact (applist (lemme,
+  exact_no_check (applist (lemme,
 		  List.map mkVar (List.rev (ids_of_var_context sign))))
     gls
 
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index d6332c553c..e7e15881d0 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -86,8 +86,11 @@ val intros_clearing      : bool list -> tactic
 val assumption         : tactic
 val dyn_assumption     : tactic_arg list -> tactic
 
-val exact              : constr -> tactic
-val dyn_exact          : tactic_arg list -> tactic
+val exact_no_check      : constr -> tactic
+val dyn_exact_no_check  : tactic_arg list -> tactic
+
+val exact_check      : constr -> tactic
+val dyn_exact_check  : tactic_arg list -> tactic
 
 (*s Reduction tactics. *)
 
diff --git a/tactics/tauto.ml b/tactics/tauto.ml
index 737ce8a33a..7e99167e71 100644
--- a/tactics/tauto.ml
+++ b/tactics/tauto.ml
@@ -81,12 +81,10 @@ let is_atomic m =
       (is_matching (get_pat pi_pattern) m)  ||
       (is_matching (not_pattern ()) m))
       
-let hypothesis = function Some id -> exact (mkVar id) | None -> assert false
-
 (* Steps of the procedure *)
 
 (* 1. A,Gamma |- A *)
-let dyck_hypothesis = compose hypothesis in_some
+let dyck_hypothesis id = exact_check (mkVar id)
 
 (* 2. False,Gamma |- G *)
 let dyck_absurdity_elim = contradiction_on_hyp
@@ -210,7 +208,7 @@ let back_thru_2 id =
 let back_thru_1 id =
   applist(mkVar id,[mkMeta(new_meta())])
 
-let exact_last_hyp = onLastHyp (fun h -> exact (mkVar (out_some h)))
+let exact_last_hyp = onLastHyp (fun h -> exact_no_check (mkVar (out_some h)))
 
 let imply_imply_bot_pattern = put_pat mmk "(?1 -> ?2) -> ?3"
 
@@ -1841,7 +1839,7 @@ let exacto tt gls =
   let tac =
     try
       let t = cci_of_tauto_term (pf_env gls) tt in
-      exact t
+      exact_no_check t
     with _ -> tAUTOFAIL     (* Efectivamente, es cualquier cosa!! *)
   in tac gls                (* Esto confirma el comentario anterior *)