diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-29 11:08:50 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-29 11:08:50 +0000 |
| commit | 392300a73bc4e57d2be865d9a8d77c608ef02f59 (patch) | |
| tree | 44b4f39e7f92f29f4626d4aa8265fe68eb129111 /tactics | |
| parent | a936f2e879ac1f9b2e7e9d8a5376469e3d53c606 (diff) | |
New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15375 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.ml | 2 | ||||
| -rw-r--r-- | tactics/extraargs.mli | 2 | ||||
| -rw-r--r-- | tactics/leminv.mli | 2 | ||||
| -rw-r--r-- | tactics/rewrite.ml4 | 2 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 1 | ||||
| -rw-r--r-- | tactics/tacinterp.mli | 2 | ||||
| -rw-r--r-- | tactics/tactics.mli | 2 |
7 files changed, 7 insertions, 6 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index f167a91a3..f580f839c 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -825,7 +825,7 @@ let prepare_hint env (sigma,c) = let path_of_constr_expr c = match c with - | Topconstr.CRef r -> (try PathHints [global r] with _ -> PathAny) + | Constrexpr.CRef r -> (try PathHints [global r] with _ -> PathAny) | _ -> PathAny let interp_hints h = diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli index 5d3691b54..ee4f38c9d 100644 --- a/tactics/extraargs.mli +++ b/tactics/extraargs.mli @@ -10,7 +10,7 @@ open Tacexpr open Term open Names open Proof_type -open Topconstr +open Constrexpr open Termops open Glob_term open Misctypes diff --git a/tactics/leminv.mli b/tactics/leminv.mli index 21fcc0f5d..fc72bd4e4 100644 --- a/tactics/leminv.mli +++ b/tactics/leminv.mli @@ -3,7 +3,7 @@ open Names open Term open Glob_term open Proof_type -open Topconstr +open Constrexpr open Misctypes val lemInv_gen : quantified_hypothesis -> constr -> tactic diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 04a1734fb..4a0d143dc 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -32,7 +32,7 @@ open Hiddentac open Typeclasses open Typeclasses_errors open Classes -open Topconstr +open Constrexpr open Pfedit open Command open Libnames diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 8e68d8e70..88767a363 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -32,6 +32,7 @@ open Proof_type open Refiner open Tacmach open Tactic_debug +open Constrexpr open Topconstr open Term open Termops diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index 861dcb97c..35e0c456b 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -16,7 +16,7 @@ open Tactic_debug open Term open Tacexpr open Genarg -open Topconstr +open Constrexpr open Mod_subst open Redexpr open Misctypes diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 40bcb94c9..5cf460366 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -118,7 +118,7 @@ val assumption : tactic val exact_no_check : constr -> tactic val vm_cast_no_check : constr -> tactic val exact_check : constr -> tactic -val exact_proof : Topconstr.constr_expr -> tactic +val exact_proof : Constrexpr.constr_expr -> tactic (** {6 Reduction tactics. } *) |