diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-06 19:12:08 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-06 19:12:08 +0000 |
| commit | 95d4aef96fb7b490b188afe66e8345428e9706ee (patch) | |
| tree | 3990c1a6bfce095e941d756df5387b63e86e8353 /pretyping/evarutil.ml | |
| parent | ef41c3d1f93e2fa82cbaa97adaa03852e8fcd7b8 (diff) | |
Paramétrisation vis à vis de existential_key
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4321 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/evarutil.ml')
| -rw-r--r-- | pretyping/evarutil.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 13ed8e8f6..bb1bfb67e 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -52,7 +52,7 @@ let filter_sign p sign x = (* Expanding existential variables (pretyping.ml) *) (* 1- whd_ise fails if an existential is undefined *) -exception Uninstantiated_evar of int +exception Uninstantiated_evar of existential_key let rec whd_ise sigma c = match kind_of_term c with @@ -92,7 +92,7 @@ let evar_env evd = Global.env_of_context evd.evar_hyps (* Generator of existential names *) let new_evar = let evar_ctr = ref 0 in - fun () -> incr evar_ctr; !evar_ctr + fun () -> incr evar_ctr; existential_of_int !evar_ctr let make_evar_instance env = fold_named_context @@ -212,7 +212,7 @@ type evar_constraint = conv_pb * constr * constr type evar_defs = { mutable evars : Evd.evar_map; mutable conv_pbs : evar_constraint list; - mutable history : (int * (loc * Rawterm.hole_kind)) list } + mutable history : (existential_key * (loc * Rawterm.hole_kind)) list } let create_evar_defs evd = { evars=evd; conv_pbs=[]; history=[] } let evars_of d = d.evars |