diff options
| author | herbelin | 2011-09-26 11:46:47 +0000 |
|---|---|---|
| committer | herbelin | 2011-09-26 11:46:47 +0000 |
| commit | 91c9a1294d236f55ff6fecdf1d763e7185590ea1 (patch) | |
| tree | b6bcf7eb8c0717d6597e6fe5777d93a74fe7d1d3 /pretyping/pretyping.mli | |
| parent | a638cba857c9a93a62f35bcceab6fa2c710805d2 (diff) | |
Moving implicit tactic support from Tacinterp to Pfedit and final evar
resolution from Tacinterp to Pretyping (close to resolve_evars) so
that final evar resolution can eventually be called from Tactics.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14496 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/pretyping.mli')
| -rw-r--r-- | pretyping/pretyping.mli | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index e1f79f36c5..47b3ec875d 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -31,6 +31,7 @@ type var_map = (identifier * Pattern.constr_under_binders) list type unbound_ltac_var_map = (identifier * identifier option) list type ltac_var_map = var_map * unbound_ltac_var_map type glob_constr_ltac_closure = ltac_var_map * glob_constr +type pure_open_constr = evar_map * constr module type S = sig @@ -65,7 +66,7 @@ sig val understand_ltac : bool -> evar_map -> env -> ltac_var_map -> - typing_constraint -> glob_constr -> evar_map * constr + typing_constraint -> glob_constr -> pure_open_constr (** Standard call to get a constr from a glob_constr, resolving implicit args *) @@ -117,3 +118,7 @@ val constr_out : Dyn.t -> constr val interp_sort : glob_sort -> sorts val interp_elimination_sort : glob_sort -> sorts_family +(** Last chance for solving evars, possibly using external solver *) +val solve_remaining_evars : bool -> bool -> + (env -> evar_map -> existential -> constr) -> + env -> evar_map -> pure_open_constr -> pure_open_constr |