From f2936eda4ab74f830a4866983d6efd99fc6683ca Mon Sep 17 00:00:00 2001 From: herbelin Date: Mon, 1 Mar 2004 14:48:06 +0000 Subject: Déplacement définition intro_pattern_expr dans Genarg MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5404 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tactics/hiddentac.ml | 1 + tactics/hiddentac.mli | 1 + tactics/inv.ml | 1 + tactics/inv.mli | 1 + tactics/tacticals.ml | 1 + tactics/tacticals.mli | 1 + tactics/tactics.ml | 1 + tactics/tactics.mli | 1 + 8 files changed, 8 insertions(+) (limited to 'tactics') 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 -- cgit v1.2.3