syntaxe AST Inversion + commentaires ocamlweb autour de $

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

19 files changed, 25 insertions, 20 deletions

diff --git a/tactics/Inv.v b/tactics/Inv.v
index 1abcdd824..62c77dc8a 100644
--- a/tactics/Inv.v
+++ b/tactics/Inv.v
@@ -68,14 +68,14 @@ Grammar vernac vernac: ast :=
 
 | der_inv_clr_with [ "Derive" "Inversion_clear"  identarg($na)
                      "with" constrarg($com) "." ]
-                    -> [(MakeInversionLemma $na $com (COMMAND (PROP{Null})))]
+                    -> [(MakeInversionLemma $na $com (CONSTR (PROP))) ]
 
 | der_inv_with_srt [ "Derive" "Inversion" identarg($na)
                      "with" constrarg($com) "Sort" sortarg($s) "." ]
                     -> [(MakeSemiInversionLemma $na $com $s)]
 
 | der_inv_with [ "Derive" "Inversion" identarg($na) "with" constrarg($com) "." ]
-                -> [(MakeSemiInversionLemma $na $com (COMMAND (PROP{Null})))]
+                -> [(MakeSemiInversionLemma $na $com (CONSTR (PROP)))]
 
 | der_inv [ "Derive" "Inversion" identarg($na) identarg($id) "." ]
            -> [(MakeSemiInversionLemmaFromHyp 1 $na $id)]
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 14df28f54..24c426d31 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*i*)
 open Util
diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli
index bbbc2b047..9215eced3 100644
--- a/tactics/autorewrite.mli
+++ b/tactics/autorewrite.mli
@@ -1,3 +1,6 @@
+
+(*i $Id$ i*)
+
 open Tacmach
 open Term
 
diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli
index 237aee4be..ef1aaa50a 100644
--- a/tactics/btermdn.mli
+++ b/tactics/btermdn.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*i*)
 open Term
diff --git a/tactics/dhyp.mli b/tactics/dhyp.mli
index de81cce91..2cbf9a827 100644
--- a/tactics/dhyp.mli
+++ b/tactics/dhyp.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*i*)
 open Names
diff --git a/tactics/dn.mli b/tactics/dn.mli
index 42c6303a0..c39ab011c 100644
--- a/tactics/dn.mli
+++ b/tactics/dn.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (* Discrimination nets. *)
 
diff --git a/tactics/elim.mli b/tactics/elim.mli
index 594dc62ea..af7d17506 100644
--- a/tactics/elim.mli
+++ b/tactics/elim.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*i*)
 open Names
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 9e19a0c04..69777da3e 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*i*)
 open Names
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 183558f60..2c45e831e 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*i*)
 open Names
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 016134307..16be20610 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*i*)
 open Util
diff --git a/tactics/inv.mli b/tactics/inv.mli
index d985bb7aa..39254c763 100644
--- a/tactics/inv.mli
+++ b/tactics/inv.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*i*)
 open Names
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 238a1a0c5..cec0be893 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -344,9 +344,11 @@ let useInversionLemma =
   let gentac =
     hide_tactic "UseInversionLemma"
       (function
-	 | [Identifier id;Command com] ->
+	 | [Identifier id; Command com] ->
              fun gls -> lemInv id (pf_interp_constr gls com) gls
-	 | l  -> anomaly "useInversionLemma" l)
+	 | [Identifier id; Constr c] ->
+             fun gls -> lemInv id c gls
+	 | _  -> anomaly "useInversionLemma")
   in 
   fun id com -> gentac [Identifier id;Command com]
 
diff --git a/tactics/nbtermdn.mli b/tactics/nbtermdn.mli
index 038af44d2..7b7da16ef 100644
--- a/tactics/nbtermdn.mli
+++ b/tactics/nbtermdn.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*i*)
 open Term
diff --git a/tactics/refine.mli b/tactics/refine.mli
index 50b08265f..86d4e9c34 100644
--- a/tactics/refine.mli
+++ b/tactics/refine.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 open Term
 open Tacmach
diff --git a/tactics/tacentries.mli b/tactics/tacentries.mli
index b364706ca..e12ed0e8c 100644
--- a/tactics/tacentries.mli
+++ b/tactics/tacentries.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*i*)
 open Proof_type
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 1f3ede393..256b007fc 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*i*)
 open Names
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 03ab3a273..335694b7c 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*i*)
 open Names
diff --git a/tactics/termdn.mli b/tactics/termdn.mli
index 8281a3179..044cbf4ff 100644
--- a/tactics/termdn.mli
+++ b/tactics/termdn.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*i*)
 open Term
diff --git a/tactics/wcclausenv.mli b/tactics/wcclausenv.mli
index b3d372f21..fedea8470 100644
--- a/tactics/wcclausenv.mli
+++ b/tactics/wcclausenv.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*i*)
 open Names