diff options
| author | Pierre-Marie Pédrot | 2017-10-30 11:40:49 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-10-30 11:43:24 +0100 |
| commit | f18502f32fb25b29cafe26340edbbcedd463c646 (patch) | |
| tree | 10947a161b1617d2f39faff4c6f0b838e634a8b1 /src | |
| parent | 71208e3eee6745ed8849bd03f66db638d9897516 (diff) | |
Fix compilation after merge of Ltac_pretype interface.
Diffstat (limited to 'src')
| -rw-r--r-- | src/tac2core.ml | 2 | ||||
| -rw-r--r-- | src/tac2interp.mli | 4 | ||||
| -rw-r--r-- | src/tac2match.ml | 2 | ||||
| -rw-r--r-- | src/tac2match.mli | 2 | ||||
| -rw-r--r-- | src/tac2tactics.ml | 2 |
5 files changed, 6 insertions, 6 deletions
diff --git a/src/tac2core.ml b/src/tac2core.ml index 1cfb34c249..9ef88a7d56 100644 --- a/src/tac2core.ml +++ b/src/tac2core.ml @@ -828,7 +828,7 @@ let open_constr_no_classes_flags () = let to_lvar ist = let open Glob_ops in let lfun = Tac2interp.set_env ist Id.Map.empty in - { empty_lvar with Glob_term.ltac_genargs = lfun } + { empty_lvar with Ltac_pretype.ltac_genargs = lfun } let gtypref kn = GTypRef (Other kn, []) diff --git a/src/tac2interp.mli b/src/tac2interp.mli index 211ac95196..21fdcd03af 100644 --- a/src/tac2interp.mli +++ b/src/tac2interp.mli @@ -20,8 +20,8 @@ val interp : environment -> glb_tacexpr -> valexpr Proofview.tactic (** {5 Cross-boundary encodings} *) -val get_env : Glob_term.unbound_ltac_var_map -> environment -val set_env : environment -> Glob_term.unbound_ltac_var_map -> Glob_term.unbound_ltac_var_map +val get_env : Ltac_pretype.unbound_ltac_var_map -> environment +val set_env : environment -> Ltac_pretype.unbound_ltac_var_map -> Ltac_pretype.unbound_ltac_var_map (** {5 Exceptions} *) diff --git a/src/tac2match.ml b/src/tac2match.ml index 7a22e91b6b..fef5647725 100644 --- a/src/tac2match.ml +++ b/src/tac2match.ml @@ -14,7 +14,7 @@ module NamedDecl = Context.Named.Declaration type context = EConstr.t type result = { - subst : Pattern.patvar_map ; + subst : Ltac_pretype.patvar_map ; } type match_pattern = diff --git a/src/tac2match.mli b/src/tac2match.mli index cf64542f40..7cfa1ed25f 100644 --- a/src/tac2match.mli +++ b/src/tac2match.mli @@ -30,4 +30,4 @@ val match_goal: match_rule -> ((Id.t * context option) list * (** List of hypotheses matching: name + context *) context option * (** Context for conclusion *) - Pattern.patvar_map (** Pattern variable substitution *)) Proofview.tactic + Ltac_pretype.patvar_map (** Pattern variable substitution *)) Proofview.tactic diff --git a/src/tac2tactics.ml b/src/tac2tactics.ml index b496f5046f..c68fdf9a7a 100644 --- a/src/tac2tactics.ml +++ b/src/tac2tactics.ml @@ -343,7 +343,7 @@ let discriminate ev arg = let injection ev ipat arg = let arg = Option.map (fun arg -> None, arg) arg in let ipat = Option.map mk_intro_patterns ipat in - let tac ev arg = Equality.injClause ipat ev arg in + let tac ev arg = Equality.injClause None ipat ev arg in on_destruction_arg tac ev arg let autorewrite ~all by ids cl = |