diff options
| author |  pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-08-09 21:57:29 +0000 |
|---|---|---|
| committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-08-09 21:57:29 +0000 |
| commit | ec3bff58d151ff804866175e907664d1fba3c600 (patch) | |
| tree | 08e546bc516217e0091fa3d19e3a829fe441b234 /pretyping/evarconv.mli | |
| parent | a234672e9d669397b40b59254c482f49007000df (diff) | |
Unification in Evar_conv uses an abstract machine state
It uses a term in front of a stack instead of a term in front of a list of applied
terms. From outside of eq_appr_x nothing should have changed.
Nasty evar instantiation bug
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15719 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/evarconv.mli')
| -rw-r--r-- | pretyping/evarconv.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 352e645fb..285c509f1 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -30,16 +30,16 @@ val evar_conv_x : transparent_state -> env -> evar_map -> conv_pb -> constr -> constr -> evar_map * bool val evar_eqappr_x : transparent_state -> env -> evar_map -> - conv_pb -> constr * constr list -> constr * constr list -> + conv_pb -> constr * constr stack -> constr * constr stack -> evar_map * bool (**/**) val consider_remaining_unif_problems : ?ts:transparent_state -> env -> evar_map -> evar_map -val check_conv_record : constr * types list -> constr * types list -> +val check_conv_record : constr * types stack -> constr * types stack -> constr * constr list * (constr list * constr list) * (constr list * types list) * - (constr list * types list) * constr * + (constr stack * types stack) * constr * (int * constr) val set_solve_evars : (env -> evar_map -> constr -> evar_map * constr) -> unit |