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 1abcdd824f..62c77dc8a0 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 14df28f548..24c426d31b 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 bbbc2b047c..9215eced30 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 237aee4be3..ef1aaa50ae 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 de81cce919..2cbf9a8270 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 42c6303a0c..c39ab011cc 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 594dc62eaf..af7d17506f 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 9e19a0c04d..69777da3e9 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 183558f601..2c45e831e0 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 0161343071..16be20610a 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 d985bb7aaf..39254c7637 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 238a1a0c51..cec0be893f 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 038af44d2d..7b7da16ef2 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 50b08265f4..86d4e9c34f 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 b364706ca1..e12ed0e8ca 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 1f3ede3938..256b007fcc 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 03ab3a2738..335694b7c9 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 8281a31799..044cbf4ff5 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 b3d372f21a..fedea84708 100644
--- a/tactics/wcclausenv.mli
+++ b/tactics/wcclausenv.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*i*)
 open Names