diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-29 11:08:53 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-29 11:08:53 +0000 |
| commit | 8a71afd27620a5d6c507b115d6fd408d879544c5 (patch) | |
| tree | 7365991d6afdfeae8529b5d47e3830b63a037a56 /tactics | |
| parent | 392300a73bc4e57d2be865d9a8d77c608ef02f59 (diff) | |
Pattern as a mli-only file, operations in Patternops
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15376 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.ml | 7 | ||||
| -rw-r--r-- | tactics/class_tactics.ml4 | 1 | ||||
| -rw-r--r-- | tactics/eauto.ml4 | 1 | ||||
| -rw-r--r-- | tactics/rewrite.ml4 | 1 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 1 | ||||
| -rw-r--r-- | tactics/termdn.ml | 1 |
6 files changed, 9 insertions, 3 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index f580f839c..158221d79 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -22,6 +22,7 @@ open Evd open Reduction open Typing open Pattern +open Patternops open Matching open Tacmach open Proof_type @@ -485,7 +486,7 @@ let make_exact_entry sigma pri ?(name=PathAny) (c,cty) = match kind_of_term cty with | Prod _ -> failwith "make_exact_entry" | _ -> - let pat = snd (Pattern.pattern_of_constr sigma cty) in + let pat = snd (Patternops.pattern_of_constr sigma cty) in let hd = try head_pattern_bound pat with BoundPattern -> failwith "make_exact_entry" @@ -502,7 +503,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri ?(name=PathAny) (c,cty) | Prod _ -> let ce = mk_clenv_from dummy_goal (c,cty) in let c' = clenv_type (* ~reduce:false *) ce in - let pat = snd (Pattern.pattern_of_constr sigma c') in + let pat = snd (Patternops.pattern_of_constr sigma c') in let hd = try head_pattern_bound pat with BoundPattern -> failwith "make_apply_entry" in @@ -576,7 +577,7 @@ let make_trivial env sigma ?(name=PathAny) c = let hd = head_of_constr_reference (fst (head_constr t)) in let ce = mk_clenv_from dummy_goal (c,t) in (Some hd, { pri=1; - pat = Some (snd (Pattern.pattern_of_constr sigma (clenv_type ce))); + pat = Some (snd (Patternops.pattern_of_constr sigma (clenv_type ce))); name = name; code=Res_pf_THEN_trivial_fail(c,t) }) diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index cafe17ad9..bfebf7810 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -24,6 +24,7 @@ open Tacmach open Evar_refiner open Tactics open Pattern +open Patternops open Clenv open Auto open Glob_term diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index e9602762d..fb692873e 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -24,6 +24,7 @@ open Tacmach open Evar_refiner open Tactics open Pattern +open Patternops open Clenv open Auto open Genredexpr diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 4a0d143dc..75f6bdb7c 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -25,6 +25,7 @@ open Tacmach open Evar_refiner open Tactics open Pattern +open Patternops open Clenv open Auto open Glob_term diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 88767a363..9b4df0ad5 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -13,6 +13,7 @@ open Declarations open Entries open Libobject open Pattern +open Patternops open Matching open Pp open Genredexpr diff --git a/tactics/termdn.ml b/tactics/termdn.ml index 5f6e5580e..0e7009113 100644 --- a/tactics/termdn.ml +++ b/tactics/termdn.ml @@ -12,6 +12,7 @@ open Names open Nameops open Term open Pattern +open Patternops open Glob_term open Libnames open Nametab |