diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-03-01 14:48:06 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-03-01 14:48:06 +0000 |
| commit | f2936eda4ab74f830a4866983d6efd99fc6683ca (patch) | |
| tree | f7fb6eb60d8496cc1319f399ceedcbca360a8f52 /tactics | |
| parent | 318110f9f690689a33b432a809e6dc62292c46e1 (diff) | |
Déplacement définition intro_pattern_expr dans Genarg
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5404 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/hiddentac.ml | 1 | ||||
| -rw-r--r-- | tactics/hiddentac.mli | 1 | ||||
| -rw-r--r-- | tactics/inv.ml | 1 | ||||
| -rw-r--r-- | tactics/inv.mli | 1 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 1 | ||||
| -rw-r--r-- | tactics/tacticals.mli | 1 | ||||
| -rw-r--r-- | tactics/tactics.ml | 1 | ||||
| -rw-r--r-- | tactics/tactics.mli | 1 |
8 files changed, 8 insertions, 0 deletions
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index 5b35fcb86..99fe569bb 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -14,6 +14,7 @@ open Tacmach open Rawterm open Refiner +open Genarg open Tacexpr open Tactics open Util diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index 364e21969..cff5dccde 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -13,6 +13,7 @@ open Names open Term open Proof_type open Tacmach +open Genarg open Tacexpr open Rawterm (*i*) diff --git a/tactics/inv.ml b/tactics/inv.ml index 2902f37e0..b9574db23 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -34,6 +34,7 @@ open Typing open Pattern open Matching open Rawterm +open Genarg open Tacexpr let collect_meta_variables c = diff --git a/tactics/inv.mli b/tactics/inv.mli index c310f7527..4c3cb00f8 100644 --- a/tactics/inv.mli +++ b/tactics/inv.mli @@ -12,6 +12,7 @@ open Names open Term open Tacmach +open Genarg open Tacexpr open Rawterm (*i*) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 486e3c3ee..bd75581aa 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -25,6 +25,7 @@ open Clenv open Pattern open Matching open Evar_refiner +open Genarg open Tacexpr (******************************************) diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 10208f738..f6b6e5b00 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -17,6 +17,7 @@ open Proof_type open Clenv open Reduction open Pattern +open Genarg open Tacexpr (*i*) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 687c5ad07..cebc6697e 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -36,6 +36,7 @@ open Tacticals open Hipattern open Coqlib open Nametab +open Genarg open Tacexpr open Decl_kinds diff --git a/tactics/tactics.mli b/tactics/tactics.mli index ee65f1332..27a7d998e 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -22,6 +22,7 @@ open Clenv open Tacred open Tacticals open Libnames +open Genarg open Tacexpr open Nametab open Rawterm |