Modification de la table des tactic Definitions pour eviter l'ecriture

de fonctions dans les .vo
ajout de lemmes dans EqNat, Logic_Type
suppression de PolyListSyntax qui redefinissait le Infix de append
Recherche d'instances a reecrire dans les Cases et les FixPoint


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

3 files changed, 58 insertions, 22 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 962073127d..f78ab96113 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -667,6 +667,12 @@ let clenv_refine_cast kONT clenv gls =
    try to find a subterm of cl which matches op, if op is just a Meta
    FAIL because we cannot find a binding *)
 
+let iter_fail f a = let n = Array.length a in 
+		    let rec ffail i = if i = n then error "iter_fail" 
+                    else try f a.(i) 
+		    with ex when catchable_exception ex -> ffail (i+1)
+		    in ffail 0
+
 let constrain_clenv_to_subterm clause (op,cl) =
   let rec matchrec cl =
     let cl = strip_outer_cast cl in
@@ -676,8 +682,11 @@ let constrain_clenv_to_subterm clause (op,cl) =
        else error "Bound 1"
      with ex when catchable_exception ex ->
        (match kind_of_term cl with 
-	  | IsApp (f,args) ->
-	      let n = Array.length args in
+	  | IsApp (f,args) ->  (try 
+		 matchrec f
+	       with ex when catchable_exception ex -> 
+		 iter_fail matchrec args)
+	(* let n = Array.length args in
 	      assert (n>0);
 	      let c1 = mkApp (f,Array.sub args 0 (n-1)) in
 	      let c2 = args.(n-1) in
@@ -685,6 +694,30 @@ let constrain_clenv_to_subterm clause (op,cl) =
 		 matchrec c1
 	       with ex when catchable_exception ex -> 
 		 matchrec c2)
+	   *)
+          | IsMutCase(_,_,c,lf) -> (* does not search in the predicate *)
+	       (try 
+		 matchrec c
+	       with ex when catchable_exception ex -> 
+		 iter_fail matchrec lf)
+	  | IsLetIn(_,c1,_,c2) -> 
+	       (try 
+		 matchrec c1
+	       with ex when catchable_exception ex -> 
+		 matchrec c2)
+
+	  | IsFix(_,(types,_,terms)) -> 
+	       (try 
+		 iter_fail matchrec types
+	       with ex when catchable_exception ex -> 
+		 iter_fail matchrec terms)
+	
+	  | IsCoFix(_,(types,_,terms)) -> 
+	       (try 
+		 iter_fail matchrec types
+	       with ex when catchable_exception ex -> 
+		 iter_fail matchrec terms)
+
           | IsProd (_,t,c) ->
 	      (try 
 		 matchrec t 
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index 09dc5a0955..22905459f5 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -156,25 +156,6 @@ let _ =
       Summary.unfreeze_function = unfreeze;
       Summary.init_function     = init }
 
-let (inMD,outMD) =
-  let add (na,td) = mactab := Gmap.add na td !mactab in
-  let cache_md (_,(na,td)) = add (na,td) in 
-    declare_object ("TACTIC-DEFINITION",
-       {cache_function         = cache_md;
-        load_function          = (fun _ -> ());
-        open_function          = (fun _ -> ());
-        specification_function = (fun x -> x)})
-
-(* Adds a Tactic Definition in the table *)
-let add_tacdef na vbody =
-  begin
-    if Gmap.mem na !mactab then
-      errorlabstrm "Tacdef.add_tacdef" 
-        [<'sTR "There is already a Tactic Definition named "; 'sTR na>];
-    let _ = Lib.add_leaf (id_of_string na) OBJ (inMD (na,vbody)) in
-    if Options.is_verbose() then mSGNL [< 'sTR (na ^ " is defined") >]
-  end
-
 (* Unboxes the tactic_arg *)
 let unvarg = function
   | VArg a -> a
@@ -956,3 +937,25 @@ let vernac_interp_atomic =
 let bad_tactic_args s =
   anomalylabstrm s
     [<'sTR "Tactic "; 'sTR s; 'sTR " called with bad arguments">]
+
+let (inMD,outMD) =
+  let add (na,td) = mactab := Gmap.add na td !mactab in
+  let cache_md (_,(na,td)) =  
+    let ve=val_interp (Evd.empty,Environ.empty_env,[],[],None,get_debug ()) td 
+    in add (na,ve) in 
+    declare_object ("TACTIC-DEFINITION",
+       {cache_function         = cache_md;
+        load_function          = cache_md;
+        open_function          = (fun _ -> ());
+        specification_function = (fun x -> x)})
+
+(* Adds a Tactic Definition in the table *)
+let add_tacdef na vbody =
+  begin
+    if Gmap.mem na !mactab then
+      errorlabstrm "Tacdef.add_tacdef" 
+        [<'sTR "There is already a Tactic Definition named "; 'sTR na>];
+    let _ = Lib.add_leaf (id_of_string na) OBJ (inMD (na,vbody)) in
+    if Options.is_verbose() then mSGNL [< 'sTR (na ^ " is defined") >]
+  end
+
diff --git a/proofs/tacinterp.mli b/proofs/tacinterp.mli
index ee5d67966a..d0ec28ea05 100644
--- a/proofs/tacinterp.mli
+++ b/proofs/tacinterp.mli
@@ -49,7 +49,7 @@ val set_debug : debug_info -> unit
 val get_debug : unit -> debug_info
 
 (* Adds a Tactic Definition in the table *)
-val add_tacdef : string -> value -> unit
+val add_tacdef : string -> Coqast.t -> unit
 
 (* Interprets any expression *)
 val val_interp : interp_sign -> Coqast.t -> value