Uniformisation convert_hyp

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

6 files changed, 38 insertions, 77 deletions

diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index 08ed476988..0d2a2f8f1a 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -1681,13 +1681,14 @@ let rec decidability gl t =
 let destructure_hyps gl =
   let rec loop evbd = function
     | [] -> (tclTHEN nat_inject coq_omega)
-    | (i,t)::lit ->
+    | (i,body,t)::lit ->
 	begin try match destructurate t with
           | Kapp(("Zle"|"Zge"|"Zgt"|"Zlt"|"Zne"),[t1;t2]) -> loop evbd lit
           | Kapp("or",[t1;t2]) ->
               (tclTHENS ((tclTHEN ((tclTHEN (elim_id i) (clear [i]))) 
 			    (intros_using [i]))) 
-		 ([ loop evbd ((i,t1)::lit); loop evbd ((i,t2)::lit) ]))
+		 ([ loop evbd ((i,None,t1)::lit);
+                    loop evbd ((i,None,t2)::lit) ]))
           | Kapp("and",[t1;t2]) ->
               let i1 = id_of_string (string_of_id i ^ "_left") in
               let i2 = id_of_string (string_of_id i ^ "_right") in
@@ -1695,7 +1696,7 @@ let destructure_hyps gl =
 		 (tclTHEN 
 		    (tclTHEN (elim_id i) (clear [i]))
 		    (intros_using [i1;i2]))
-		 (loop (i1::i2::evbd) ((i1,t1)::(i2,t2)::lit)))
+		 (loop (i1::i2::evbd) ((i1,None,t1)::(i2,None,t2)::lit)))
           | Kimp(t1,t2) ->
               if isprop (pf_type_of gl t1) & closed0 t2 then begin
 		(tclTHEN 
@@ -1707,7 +1708,7 @@ let destructure_hyps gl =
 						    mkVar i|])]) 
 			 (clear [i])) 
 		      (intros_using [i])) 
-		   (loop evbd ((i,mk_or (mk_not t1) t2)::lit)))
+		   (loop evbd ((i,None,mk_or (mk_not t1) t2)::lit)))
               end else loop evbd lit
           | Kapp("not",[t]) -> 
               begin match destructurate t with 
@@ -1719,7 +1720,7 @@ let destructure_hyps gl =
 							t1; t2; mkVar i |])])
 			     (clear [i])) 
 			  (intros_using [i])) 
-                       (loop evbd ((i,mk_and (mk_not t1) (mk_not t2)):: lit)))
+                       (loop evbd ((i,None,mk_and (mk_not t1) (mk_not t2)):: lit)))
 		| Kapp("and",[t1;t2]) -> 
                     (tclTHEN 
 		       (tclTHEN 
@@ -1729,7 +1730,7 @@ let destructure_hyps gl =
 					   decidability gl t1;mkVar i|])])
 			     (clear [i]))
 			  (intros_using [i]))
-                       (loop evbd ((i,mk_or (mk_not t1) (mk_not t2))::lit)))
+                       (loop evbd ((i,None,mk_or (mk_not t1) (mk_not t2))::lit)))
 		| Kimp(t1,t2) ->
                     (tclTHEN 
 		       (tclTHEN 
@@ -1739,7 +1740,7 @@ let destructure_hyps gl =
 					   decidability gl t1;mkVar i |])])
 			     (clear [i])) 
 			  (intros_using [i]))
-                       (loop evbd ((i,mk_and t1 (mk_not t2)) :: lit)))
+                       (loop evbd ((i,None,mk_and t1 (mk_not t2)) :: lit)))
 		| Kapp("not",[t]) ->
                     (tclTHEN 
 		       (tclTHEN 
@@ -1749,7 +1750,7 @@ let destructure_hyps gl =
 					    decidability gl t; mkVar i |])])
 			     (clear [i])) 
 			  (intros_using [i])) 
-                       (loop evbd ((i,t)::lit)))
+                       (loop evbd ((i,None,t)::lit)))
 		| Kapp("Zle", [t1;t2]) ->
                     (tclTHEN 
 		       (tclTHEN 
@@ -1852,13 +1853,15 @@ let destructure_hyps gl =
 		      match destructurate (pf_nf gl typ) with
 			| Kapp("nat",_) -> 
                             (tclTHEN 
-			       (convert_hyp i 
-				  (mkApp (Lazy.force coq_neq, [| t1;t2|])))
+			       (convert_hyp
+                                  (i,body,
+				  (mkApp (Lazy.force coq_neq, [| t1;t2|]))))
 			       (loop evbd lit))
 			| Kapp("Z",_) ->
                             (tclTHEN 
-			       (convert_hyp i 
-				  (mkApp (Lazy.force coq_Zne, [| t1;t2|])))
+			       (convert_hyp
+                                  (i,body,
+				  (mkApp (Lazy.force coq_Zne, [| t1;t2|]))))
 			       (loop evbd lit))
 			| _ -> loop evbd lit
                     end
@@ -1868,7 +1871,7 @@ let destructure_hyps gl =
 	with e when catchable_exception e -> loop evbd lit
 	end 
   in
-  loop (pf_ids_of_hyps gl) (pf_hyps_types gl) gl
+  loop (pf_ids_of_hyps gl) (pf_hyps gl) gl
 
 let destructure_goal gl =
   let concl = pf_concl gl in
diff --git a/proofs/logic.ml b/proofs/logic.ml
index cf6df42ce9..ec998ba83d 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -390,37 +390,14 @@ let error_use_instantiate () =
     (str"cannot intro when there are open metavars in the domain type" ++
        spc () ++ str"- use Instantiate")
 
-let convert_hyp sign sigma id b =
+let convert_hyp sign sigma (id,b,bt as d) =
   apply_to_hyp sign id
-    (fun sign (idc,c,ct) _ ->
+    (fun sign (_,c,ct) _ ->
        let env = Global.env_of_context sign in
-       match c with
-	 | None -> (* Change the type *)
-	     if !check && not (is_conv env sigma b ct) then
-	       error "convert-hyp rule passed non-converting term";
-	     add_named_decl (idc,c,b) sign
-	 | Some c -> (* Change the body *)
-	     if !check && not (is_conv env sigma b c) then
-	       error "convert-hyp rule passed non-converting term";
-	     add_named_decl (idc,Some b,ct) sign)
-
-let convert_def inbody sign sigma id c =
-  apply_to_hyp sign id
-    (fun sign (idc,b,t) _ ->
-       let env = Global.env_of_context sign in
-       match b with
-	 | None -> error "convert-deftype rule passed to an hyp without body" 
-	 | Some b ->
-	     let b,t = 
-	       if inbody then
-		 (if !check && not (is_conv env sigma c b) then 
-		    error "convert-deftype rule passed non-converting type";
-		  (c,t))
-	       else
-		 (if !check && not (is_conv env sigma c t) then
-		    error "convert-deftype rule passed non-converting type";
-		  (b,c)) in
-	     add_named_decl (idc,Some b,t) sign)
+       if !check && not (is_conv env sigma bt ct) &&
+         not (option_compare (is_conv env sigma) b c) then
+	   error "convert-hyp rule passed non-converting term";
+       add_named_decl d sign)
 
 
 (***********************************************************************)
@@ -584,14 +561,15 @@ let prim_refiner r sigma goal =
 	else 
 	  error "convert-concl rule passed non-converting term"
 
+(*
     | { name = Convert_hyp; hypspecs = [id]; terms = [ty] } ->
 	[mk_goal (convert_hyp sign sigma id ty) cl]
+*)
+    | { name = Convert_hyp; hypspecs = [id]; terms = [c;ty] } ->
+	[mk_goal (convert_hyp sign sigma (id,Some c,ty)) cl]
 
-    | { name = Convert_defbody; hypspecs = [id]; terms = [c] } ->
-	[mk_goal (convert_def true sign sigma id c) cl]
-
-    | { name = Convert_deftype; hypspecs = [id]; terms = [ty] } ->
-	[mk_goal (convert_def false sign sigma id ty) cl]
+    | { name = Convert_hyp; hypspecs = [id]; terms = [ty] } ->
+	[mk_goal (convert_hyp sign sigma (id,None,ty)) cl]
 
     (* And now the structural rules *)
     | { name = Thin; hypspecs = ids } -> [clear_hyps ids goal]
@@ -706,15 +684,9 @@ let prim_extractor subfun vl pft =
     | {ref=Some(Prim{name=Convert_concl;terms=[c]},[pf])} ->
 	subfun vl pf
 	
-    | {ref=Some(Prim{name=Convert_hyp;hypspecs=[id];terms=[_]},[pf])} ->
-	subfun vl pf
-
-    | {ref=Some(Prim{name=Convert_defbody;hypspecs=[id];terms=[_]},[pf])} ->
+    | {ref=Some(Prim{name=Convert_hyp;hypspecs=[id];terms=_},[pf])} ->
 	subfun vl pf
 
-    | {ref=Some(Prim{name=Convert_deftype;hypspecs=[id];terms=[_]},[pf])} ->
-	subfun vl pf
-	
     | {ref=Some(Prim{name=Thin;hypspecs=ids},[pf])} ->
      (* No need to make ids Anonymous in vl: subst_vars take the more recent *)
 	subfun vl pf
@@ -788,13 +760,10 @@ let pr_prim_rule = function
       
   | {name=Convert_hyp;hypspecs=[id];terms=[c]} ->
       (str"Change "  ++ prterm c  ++ spc ()  ++ str"in "  ++ pr_id id)
-      
-  | {name=Convert_defbody;hypspecs=[id];terms=[c]} ->
-      (str"Change "  ++ prterm c  ++ spc ()  ++ str"in "  ++ pr_id id)
 
-  | {name=Convert_deftype;hypspecs=[id];terms=[c]} ->
-      (str"Change "  ++ prterm c  ++ spc ()  ++
-	 str"in (Type of "  ++ pr_id id ++ str ")")
+  | {name=Convert_hyp;hypspecs=[id];terms=[c;t]} ->
+      (str"Change "  ++ prterm c  ++ spc ()  ++ str"in "
+       ++ pr_id id ++ str" (Type of "  ++ pr_id id ++ str ")")
       
   | {name=Thin;hypspecs=ids} ->
       (str"Clear "  ++ prlist_with_sep pr_spc pr_id ids)
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index f1df084b2b..c84a147d9b 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -41,8 +41,6 @@ type prim_rule_name =
   | Refine 
   | Convert_concl
   | Convert_hyp
-  | Convert_defbody
-  | Convert_deftype
   | Thin
   | ThinBody
   | Move of bool
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index dd6f0f05d9..bbee9b3533 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -44,8 +44,6 @@ type prim_rule_name =
   | Refine 
   | Convert_concl
   | Convert_hyp
-  | Convert_defbody
-  | Convert_deftype
   | Thin
   | ThinBody
   | Move of bool
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 362bac2a60..f331c3537f 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -235,17 +235,12 @@ let convert_concl c pf =
   refiner (Prim { name = Convert_concl; terms = [c];
                   hypspecs = []; newids = []; params = [] }) pf
 
-let convert_hyp id t pf =
+let convert_hyp (id,b,t) pf =
+  let lt = match b with
+    | None -> [t]
+    | Some c -> [c;t] in
   refiner (Prim { name = Convert_hyp; hypspecs = [id];
-                  terms = [t]; newids = []; params = []}) pf
-
-let convert_defbody id t pf =
-  refiner (Prim { name = Convert_defbody; hypspecs = [id];
-                  terms = [t]; newids = []; params = []}) pf
-
-let convert_deftype id t pf =
-  refiner (Prim { name = Convert_deftype; hypspecs = [id];
-                  terms = [t]; newids = []; params = []}) pf
+                  terms = lt; newids = []; params = []}) pf
 
 let thin ids gl = 
   refiner (Prim { name = Thin; hypspecs = ids;
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index eba872a772..d40016e505 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -157,9 +157,7 @@ val internal_cut    : identifier -> types -> tactic
 val internal_cut_rev : identifier -> types -> tactic
 val refine          : constr -> tactic
 val convert_concl   : types -> tactic
-val convert_hyp     : identifier -> types -> tactic
-val convert_deftype : identifier -> types -> tactic
-val convert_defbody : identifier -> constr -> tactic
+val convert_hyp     : named_declaration -> tactic
 val thin            : identifier list -> tactic
 val thin_body       : identifier list -> tactic
 val move_hyp        : bool -> identifier -> identifier -> tactic