diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/btermdn.ml | 2 | ||||
| -rw-r--r-- | tactics/class_tactics.ml | 8 | ||||
| -rw-r--r-- | tactics/contradiction.ml | 2 | ||||
| -rw-r--r-- | tactics/eauto.ml | 2 | ||||
| -rw-r--r-- | tactics/eqdecide.ml | 2 | ||||
| -rw-r--r-- | tactics/equality.ml | 1 | ||||
| -rw-r--r-- | tactics/hints.ml | 9 | ||||
| -rw-r--r-- | tactics/hints.mli | 10 | ||||
| -rw-r--r-- | tactics/hipattern.ml | 2 | ||||
| -rw-r--r-- | tactics/inv.ml | 1 | ||||
| -rw-r--r-- | tactics/leminv.ml | 2 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 4 | ||||
| -rw-r--r-- | tactics/term_dnet.ml | 2 |
14 files changed, 25 insertions, 24 deletions
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index 8f50b0aa2..aca7f6c65 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -9,7 +9,7 @@ (************************************************************************) open Util -open Term +open Constr open EConstr open Names open Pattern diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 3e08c6d87..998efdd6d 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -18,6 +18,7 @@ open CErrors open Util open Names open Term +open Constr open Termops open EConstr open Tacmach @@ -546,12 +547,7 @@ let make_resolve_hyp env sigma st flags only_classes pri decl = let hints = build_subclasses ~check:false env sigma (VarRef id) empty_hint_info in (List.map_append (fun (path,info,c) -> - let info = - { info with hint_pattern = - Option.map (Constrintern.intern_constr_pattern env sigma) - info.hint_pattern } - in - make_resolves env sigma ~name:(PathHints path) + make_resolves env sigma ~name:(PathHints path) (true,false,not !Flags.quiet) info false (IsConstr (EConstr.of_constr c,Univ.ContextSet.empty))) hints) diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index c285f21e7..b92bc75bc 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Term +open Constr open EConstr open Hipattern open Tactics diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 3df9e3f82..80d07c5c0 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -12,7 +12,7 @@ open Pp open CErrors open Util open Names -open Term +open Constr open Termops open EConstr open Proof_type diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index b0deeed17..176701d99 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -17,7 +17,7 @@ open Util open Names open Namegen -open Term +open Constr open EConstr open Declarations open Tactics diff --git a/tactics/equality.ml b/tactics/equality.ml index 8904cd170..f9e06391a 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -15,6 +15,7 @@ open Util open Names open Nameops open Term +open Constr open Termops open EConstr open Vars diff --git a/tactics/hints.ml b/tactics/hints.ml index 29744e406..a86103d57 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -12,7 +12,7 @@ open Pp open Util open CErrors open Names -open Term +open Constr open Evd open EConstr open Vars @@ -23,7 +23,6 @@ open Libobject open Namegen open Libnames open Smartlocate -open Misctypes open Termops open Inductiveops open Typing @@ -100,6 +99,8 @@ let empty_hint_info = (* The Type of Constructions Autotactic Hints *) (************************************************************************) +type hint_info_expr = Constrexpr.constr_pattern_expr hint_info_gen + type 'a hint_ast = | Res_pf of 'a (* Hint Apply *) | ERes_pf of 'a (* Hint EApply *) @@ -165,7 +166,7 @@ type hint_mode = | ModeOutput (* Anything *) type hints_expr = - | HintsResolve of (Typeclasses.hint_info_expr * bool * reference_or_constr) list + | HintsResolve of (hint_info_expr * bool * reference_or_constr) list | HintsImmediate of reference_or_constr list | HintsUnfold of reference list | HintsTransparency of reference list * bool @@ -1235,7 +1236,7 @@ let add_trivials env sigma l local dbnames = type hnf = bool -type hint_info = (patvar list * constr_pattern) hint_info_gen +type nonrec hint_info = hint_info type hints_entry = | HintsResolveEntry of (hint_info * polymorphic * hnf * hints_path_atom * hint_term) list diff --git a/tactics/hints.mli b/tactics/hints.mli index f05988703..7ef7f0185 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -14,10 +14,10 @@ open EConstr open Environ open Decl_kinds open Evd -open Misctypes open Tactypes open Clenv open Pattern +open Typeclasses (** {6 General functions. } *) @@ -33,6 +33,8 @@ val empty_hint_info : 'a Typeclasses.hint_info_gen (** Pre-created hint databases *) +type hint_info_expr = Constrexpr.constr_pattern_expr hint_info_gen + type 'a hint_ast = | Res_pf of 'a (* Hint Apply *) | ERes_pf of 'a (* Hint EApply *) @@ -80,7 +82,7 @@ type hint_mode = | ModeOutput (* Anything *) type hints_expr = - | HintsResolve of (Typeclasses.hint_info_expr * bool * reference_or_constr) list + | HintsResolve of (hint_info_expr * bool * reference_or_constr) list | HintsImmediate of reference_or_constr list | HintsUnfold of Libnames.reference list | HintsTransparency of Libnames.reference list * bool @@ -160,8 +162,6 @@ type hint_db = Hint_db.t type hnf = bool -type hint_info = (patvar list * constr_pattern) Typeclasses.hint_info_gen - type hint_term = | IsGlobRef of GlobRef.t | IsConstr of constr * Univ.ContextSet.t @@ -290,3 +290,5 @@ val pr_hint : env -> evar_map -> hint -> Pp.t (** Hook for changing the initialization of auto *) val add_hints_init : (unit -> unit) -> unit +type nonrec hint_info = hint_info +[@@ocaml.deprecated "Use [Typeclasses.hint_info]"] diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index b8f1ed720..5d264058a 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -12,7 +12,7 @@ open Pp open CErrors open Util open Names -open Term +open Constr open Termops open EConstr open Inductiveops diff --git a/tactics/inv.ml b/tactics/inv.ml index b346ed223..28cfd57a2 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -14,6 +14,7 @@ open Util open Names open Term open Termops +open Constr open EConstr open Vars open Namegen diff --git a/tactics/leminv.ml b/tactics/leminv.ml index a4cdc1592..f47e6b2cd 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -12,9 +12,9 @@ open Pp open CErrors open Util open Names -open Term open Termops open Environ +open Constr open EConstr open Vars open Namegen diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 6c7db26c7..732d06f8a 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -509,7 +509,7 @@ module New = struct match Evd.evar_body evi with | Evd.Evar_empty -> Some (evk,evi) | Evd.Evar_defined c -> match Constr.kind (EConstr.Unsafe.to_constr c) with - | Term.Evar (evk,l) -> is_undefined_up_to_restriction sigma evk + | Evar (evk,l) -> is_undefined_up_to_restriction sigma evk | _ -> (* We make the assumption that there is no way to refine an evar remaining after typing from the initial term given to diff --git a/tactics/tactics.ml b/tactics/tactics.ml index bb57e2bf4..58c62af85 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1910,8 +1910,8 @@ let cast_no_check cast c = exact_no_check (mkCast (c, cast, concl)) end -let vm_cast_no_check c = cast_no_check Term.VMcast c -let native_cast_no_check c = cast_no_check Term.NATIVEcast c +let vm_cast_no_check c = cast_no_check VMcast c +let native_cast_no_check c = cast_no_check NATIVEcast c let exact_proof c = let open Tacmach.New in diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml index 611799990..8bdcc6321 100644 --- a/tactics/term_dnet.ml +++ b/tactics/term_dnet.ml @@ -290,7 +290,7 @@ struct | Const (c,u) -> Term (DRef (ConstRef c)) | Ind (i,u) -> Term (DRef (IndRef i)) | Construct (c,u)-> Term (DRef (ConstructRef c)) - | Term.Meta _ -> assert false + | Meta _ -> assert false | Evar (i,_) -> let meta = try Evar.Map.find i !metas |