Add a type argument to letin_tac instead of using casts and recomputing

when one wants a particular type. Rewrite of the unification behind
[Equations], much more robust but still buggy w.r.t. inaccessible
patterns.


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

7 files changed, 18 insertions, 18 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 22e95ef5d8..f5b0355f5a 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -800,7 +800,7 @@ let refresh_hypinfo env sigma hypinfo =
       match c with 
 	| Some c ->
 	    (* Refresh the clausenv to not get the same meta twice in the goal. *)
-	    hypinfo := decompose_setoid_eqhyp cl.env (Evd.evars_of cl.evd) c l2r;
+	    hypinfo := decompose_setoid_eqhyp env (Evd.evars_of cl.evd) c l2r;
 	| _ -> ()
   else ()
 
@@ -1054,7 +1054,7 @@ let cl_rewrite_clause_aux ?(flags=default_flags) hypinfo goal_meta occs clause g
   let sigma = project gl in
   let eq = build_new gl env sigma flags occs hypinfo concl (Some (Lazy.lazy_from_val cstr)) evars 
   in
-    match eq with  
+    match eq with
     | Some (p, (_, _, oldt, newt)) -> 
 	(try 
 	  evars := Typeclasses.resolve_typeclasses env ~split:false ~fail:true !evars;
@@ -1842,7 +1842,7 @@ let rec head_of_constr t =
 TACTIC EXTEND head_of_constr
   [ "head_of_constr" ident(h) constr(c) ] -> [
     let c = head_of_constr c in
-      letin_tac None (Name h) c allHyps
+      letin_tac None (Name h) c None allHyps
   ]
 END
 
@@ -1938,8 +1938,8 @@ let varify_constr_varmap ty def varh c =
 TACTIC EXTEND varify
   [ "varify" ident(varh) ident(h') constr(ty) constr(def) constr(c) ] -> [
     let vars, c' = varify_constr_varmap ty def (mkVar varh) c in
-      tclTHEN (letin_tac None (Name varh) vars allHyps)
-	(letin_tac None (Name h') c' allHyps)
+      tclTHEN (letin_tac None (Name varh) vars None allHyps)
+	(letin_tac None (Name h') c' None allHyps)
   ]
 END
 
diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml
index 3b45573f8d..299e3fd17b 100644
--- a/tactics/decl_proof_instr.ml
+++ b/tactics/decl_proof_instr.ml
@@ -264,7 +264,7 @@ let add_justification_hyps keep items gls =
       | _ -> 
 	  let id=pf_get_new_id local_hyp_prefix gls in 
 	    keep:=Idset.add id !keep; 
-	    tclTHEN (letin_tac None (Names.Name id) c Tacexpr.nowhere)
+	    tclTHEN (letin_tac None (Names.Name id) c None Tacexpr.nowhere)
               (thin_body [id]) gls in 
     tclMAP add_aux items gls   
 
@@ -811,7 +811,7 @@ let rec build_function args body =
 
 let define_tac id args body gls =
   let t = build_function args body in
-    letin_tac None (Name id) t Tacexpr.nowhere gls
+    letin_tac None (Name id) t None Tacexpr.nowhere gls
 
 (* tactics for reconsider *)
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index cceda72f99..9994bd7848 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1213,8 +1213,8 @@ let subst_one x gl =
       (id,None,_) -> intro_using id
     | (id,Some hval,htyp) ->
         letin_tac None (Name id)
-	  (mkCast(replace_term varx rhs hval,DEFAULTcast,
-	          replace_term varx rhs htyp)) nowhere
+	  (replace_term varx rhs hval)
+	  (Some (replace_term varx rhs htyp)) nowhere
   in
   let need_rewrite = dephyps <> [] || depconcl in
   tclTHENLIST 
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index 8313a09475..5e87d432ba 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -75,5 +75,5 @@ let let_evar name typ gls =
   let evd = Evd.create_goal_evar_defs gls.sigma in
   let evd',evar = Evarutil.new_evar evd (pf_env gls) typ in
   Refiner.tclTHEN (Refiner.tclEVARS (evars_of evd'))
-    (Tactics.letin_tac None name evar nowhere) gls
+    (Tactics.letin_tac None name evar None nowhere) gls
  
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 4283720039..1acc4880c1 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -71,7 +71,7 @@ let h_generalize_dep c =
   abstract_tactic (TacGeneralizeDep (inj_open c))(generalize_dep c)
 let h_let_tac b na c cl =
   let with_eq = if b then None else Some (true,(dummy_loc,IntroAnonymous)) in
-  abstract_tactic (TacLetTac (na,inj_open c,cl,b)) (letin_tac with_eq na c cl)
+  abstract_tactic (TacLetTac (na,inj_open c,cl,b)) (letin_tac with_eq na c None cl)
 let h_instantiate n c ido = 
 (Evar_tactics.instantiate n c ido)
   (* abstract_tactic (TacInstantiate (n,c,cls))
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2162d891a5..36ec22ee61 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1404,14 +1404,14 @@ let letin_abstract id c occs gl =
     if depdecls = [] then no_move else MoveAfter(pi1(list_last depdecls)) in
   (depdecls,lastlhyp,ccl)
 
-let letin_tac with_eq name c occs gl =
+let letin_tac with_eq name c ty occs gl =
   let id =
     let x = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c) name in
     if name = Anonymous then fresh_id [] x gl else
       if not (mem_named_context x (pf_hyps gl)) then x else
 	error ("The variable "^(string_of_id x)^" is already declared.") in
   let (depdecls,lastlhyp,ccl)= letin_abstract id c occs gl in 
-  let t = pf_type_of gl c in
+  let t = match ty with Some t -> t | None -> pf_type_of gl c in
   let newcl,eq_tac = match with_eq with
     | Some (lr,(loc,ido)) ->
       let heq = match ido with
@@ -1618,14 +1618,14 @@ let atomize_param_of_ind (indref,nparams) hyp0 gl =
 	| Var id ->
 	    let x = fresh_id [] id gl in
 	    tclTHEN
-	      (letin_tac None (Name x) (mkVar id) allClauses)
+	      (letin_tac None (Name x) (mkVar id) None allClauses)
 	      (atomize_one (i-1) ((mkVar x)::avoid)) gl
 	| _ ->
 	    let id = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c)
 		       Anonymous in
 	    let x = fresh_id [] id gl in
 	    tclTHEN
-	      (letin_tac None (Name x) c allClauses)
+	      (letin_tac None (Name x) c None allClauses)
 	      (atomize_one (i-1) ((mkVar x)::avoid)) gl
     else 
       tclIDTAC gl
@@ -2558,7 +2558,7 @@ let new_induct_gen isrec with_evars elim (eqname,names) (c,lbind) cls gl =
 	  | _ ->
 	    if cls <> None then Some (false,(dloc,IntroAnonymous)) else None in
 	tclTHEN
-	  (letin_tac with_eq (Name id) c (Option.default allClauses cls))
+	  (letin_tac with_eq (Name id) c None (Option.default allClauses cls))
 	  (induction_with_atomization_of_ind_arg
 	     isrec with_evars elim names (id,lbind)) gl
 
@@ -2592,7 +2592,7 @@ let new_induct_gen_l isrec with_evars elim (eqname,names) lc gl =
 		let _ = newlc:=id::!newlc in
 		let _ = letids:=id::!letids in
 		tclTHEN 
-		  (letin_tac None (Name id) c allClauses)
+		  (letin_tac None (Name id) c None allClauses)
 		  (atomize_list newl') gl in
   tclTHENLIST 
     [
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index d3d353f172..58df7155e7 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -349,7 +349,7 @@ val cut_in_parallel             : constr list -> tactic
 val assert_as : bool -> intro_pattern_expr located -> constr -> tactic
 val forward   : tactic option -> intro_pattern_expr located -> constr -> tactic
 val letin_tac : (bool * intro_pattern_expr located) option -> name -> 
-  constr -> clause -> tactic
+  constr -> types option -> clause -> tactic
 val true_cut                    : name -> constr -> tactic
 val assert_tac                  : bool -> name -> constr -> tactic
 val generalize      : constr list -> tactic