diff options
author | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
commit | 208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch) | |
tree | 591e9e512063e34099782e2518573f15ffeac003 /pretyping/evarutil.mli | |
parent | de0085539583f59dc7c4bf4e272e18711d565466 (diff) |
Imported Upstream version 8.1~gammaupstream/8.1.gamma
Diffstat (limited to 'pretyping/evarutil.mli')
-rw-r--r-- | pretyping/evarutil.mli | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 7429cd16..3ac05481 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: evarutil.mli 8695 2006-04-10 16:33:52Z msozeau $ i*) +(*i $Id: evarutil.mli 9141 2006-09-15 10:07:01Z herbelin $ i*) (*i*) open Util @@ -78,10 +78,18 @@ val solve_simple_eqn : -> env -> evar_defs -> conv_pb * existential * constr -> evar_defs * bool +(* [check_evars env initial_sigma extended_sigma c] fails if some + new unresolved evar remains in [c] *) +val check_evars : env -> evar_map -> evar_defs -> constr -> unit + val define_evar_as_arrow : evar_defs -> existential -> evar_defs * types val define_evar_as_lambda : evar_defs -> existential -> evar_defs * types val define_evar_as_sort : evar_defs -> existential -> evar_defs * sorts +val is_unification_pattern_evar : existential -> constr list -> bool +val is_unification_pattern : constr -> constr array -> bool +val solve_pattern_eqn : env -> constr list -> constr -> constr + (***********************************************************) (* Value/Type constraints *) |