diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-25 18:34:53 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:30:41 +0100 |
| commit | 02dd160233adc784eac732d97a88356d1f0eaf9b (patch) | |
| tree | d2baacdc2a4ae06e4607bfe09b48ba2c23a78a0f /pretyping/pretyping.mli | |
| parent | a5499688bd76def8de3d8e1089a49c7a08430903 (diff) | |
Removing various compatibility layers of tactics.
Diffstat (limited to 'pretyping/pretyping.mli')
| -rw-r--r-- | pretyping/pretyping.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index a1602088a..825d73f1f 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -76,10 +76,10 @@ val allow_anonymous_refs : bool ref evar_map is modified explicitly or by side-effect. *) val understand_tcc : ?flags:inference_flags -> env -> evar_map -> - ?expected_type:typing_constraint -> glob_constr -> open_constr + ?expected_type:typing_constraint -> glob_constr -> evar_map * EConstr.constr val understand_tcc_evars : ?flags:inference_flags -> env -> evar_map ref -> - ?expected_type:typing_constraint -> glob_constr -> constr + ?expected_type:typing_constraint -> glob_constr -> EConstr.constr (** More general entry point with evars from ltac *) @@ -95,7 +95,7 @@ val understand_tcc_evars : ?flags:inference_flags -> env -> evar_map ref -> val understand_ltac : inference_flags -> env -> evar_map -> ltac_var_map -> - typing_constraint -> glob_constr -> pure_open_constr + typing_constraint -> glob_constr -> evar_map * EConstr.constr (** Standard call to get a constr from a glob_constr, resolving implicit arguments and coercions, and compiling pattern-matching; |