diff options
| author | msozeau | 2012-03-19 17:48:52 +0000 |
|---|---|---|
| committer | msozeau | 2012-03-19 17:48:52 +0000 |
| commit | 8686e11304bdeb7a4f04629b0643098f60a19739 (patch) | |
| tree | 8134cb674fd7dee6be4fd61308edb29d4e66ba45 /pretyping | |
| parent | e5320fdb6a60b6593458ea123a74f5cc31cf8df4 (diff) | |
Fix bugs related to Program integration.
- reinstall (x : T | P) binder syntax extension.
- fix a wrong Evd.define in coercion code.
- Simplify interface of eterm_obligations to take a single evar_map.
- Fix a slightly subtle bug related to resolvability of evars: some
were marked unresolvable and never set back to resolvable across calls
to typeclass resolution.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15057 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 2 | ||||
| -rw-r--r-- | pretyping/coercion.ml | 10 | ||||
| -rw-r--r-- | pretyping/typeclasses.ml | 3 | ||||
| -rw-r--r-- | pretyping/typeclasses.mli | 1 |
4 files changed, 11 insertions, 5 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 0f77053179..871f161abd 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -337,6 +337,8 @@ let coerce_row typing_fun evdref env pats (tomatch,(_,indopt)) = let loc = Some (loc_of_glob_constr tomatch) in let tycon,realnames = find_tomatch_tycon evdref env loc indopt in let j = typing_fun tycon env evdref tomatch in + let evd, j = Coercion.inh_coerce_to_base (loc_of_glob_constr tomatch) env !evdref j in + evdref := evd; let typ = nf_evar !evdref j.uj_type in let t = try try_find_ind env !evdref typ realnames diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 2b93a5fca8..3277456163 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -219,8 +219,11 @@ and coerce loc env isevars (x : Term.constr) (y : Term.constr) let (evs, t) = Evarutil.define_evar_as_lambda env !isevars (k,args) in isevars := evs; let (n, dom, rng) = destLambda t in - let (domk, args) = destEvar dom in - isevars := define domk a !isevars; + let dom = whd_evar !isevars dom in + if isEvar dom then + let (domk, args) = destEvar dom in + isevars := define domk a !isevars; + else (); t, rng | _ -> raise NoSubtacCoercion in @@ -228,8 +231,7 @@ and coerce loc env isevars (x : Term.constr) (y : Term.constr) let env' = push_rel (make_name "x", None, a) env in let c2 = coerce_unify env' b b' in match c1, c2 with - None, None -> - None + | None, None -> None | _, _ -> Some (fun x -> diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 8fe06539c6..be335ac913 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -480,9 +480,10 @@ let mark_resolvability_undef b evi = let mark_resolvability b evi = assert (evi.evar_body = Evar_empty); - mark_resolvability_undef false evi + mark_resolvability_undef b evi let mark_unresolvable evi = mark_resolvability false evi +let mark_resolvable evi = mark_resolvability true evi let mark_resolvability b sigma = Evd.fold_undefined (fun ev evi evs -> diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 3d36168fd1..67336b3407 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -85,6 +85,7 @@ val instance_constructor : typeclass -> constr list -> constr option * types val is_resolvable : evar_info -> bool val mark_unresolvable : evar_info -> evar_info val mark_unresolvables : evar_map -> evar_map +val mark_resolvable : evar_info -> evar_info val mark_resolvables : evar_map -> evar_map val is_class_evar : evar_map -> evar_info -> bool |