diff options
| author |  puech <puech@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-09 16:05:34 +0000 |
|---|---|---|
| committer | puech <puech@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-09 16:05:34 +0000 |
| commit | 2e6c3a7b0b12cfd3b560de60f4918063f149fd01 (patch) | |
| tree | c7dc3dfce59e43a01835278fd59c303373b3dd50 | |
| parent | 7f8fb01ffcaa6aeafef0cea9d7169d70ce841537 (diff) | |
* Fixed constr_cmp again to handle universes subtyping correctly
* Fixed typo in unify_0 regarding conv_pb
* First attempt to fix a problem related to rels in w_merge. Seems to
be unsuccessful at this point
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11443 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/termops.ml | 13 | ||||
| -rw-r--r-- | pretyping/unification.ml | 9 |
2 files changed, 11 insertions, 11 deletions
diff --git a/pretyping/termops.ml b/pretyping/termops.ml index d18ee4fde..7cbde2d07 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -946,13 +946,12 @@ let base_sort_cmp pb s0 s1 = (* eq_constr extended with universe erasure *) let rec constr_cmp cv_pb t1 t2 = - (match kind_of_term t1, kind_of_term t2 with - Sort s1, Sort s2 -> base_sort_cmp cv_pb s1 s2 - | Prod (_,t1,c1), Prod (_,t2,c2) -> - constr_cmp Reduction.CONV t1 t2 & - constr_cmp cv_pb c1 c2 - | _ -> false) - || compare_constr (constr_cmp Reduction.CONV) t1 t2 + match kind_of_term t1, kind_of_term t2 with + Sort s1, Sort s2 -> base_sort_cmp cv_pb s1 s2 + | Prod (_,t1,c1), Prod (_,t2,c2) -> + constr_cmp Reduction.CONV t1 t2 & + constr_cmp cv_pb c1 c2 + | _ -> compare_constr (constr_cmp Reduction.CONV) t1 t2 let eq_constr = constr_cmp Reduction.CONV diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 85e775f2a..a2671b5d1 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -172,7 +172,7 @@ let unify_0_with_initial_metas subst conv_at_top env sigma cv_pb flags m n = (match flags.modulo_conv_on_closed_terms with Some flags -> is_trans_fconv (conv_pb_of pb) flags env sigma m n - | None -> constr_cmp (conv_pb_of cv_pb) m n) + | None -> constr_cmp (conv_pb_of pb) m n) | _ -> constr_cmp (conv_pb_of cv_pb) m n in let rec unirec_rec curenv pb b ((metasubst,evarsubst) as substn) curm curn = let cM = Evarutil.whd_castappevar sigma curm @@ -522,9 +522,10 @@ let w_merge env with_types flags (metas,evars) evd = w_merge_rec evd' metas evars eqns | _ -> let evi = Evd.find (evars_of evd) evn in - let rty = Retyping.get_type_of_with_meta env (evars_of evd) (metas_of evd) rhs' in - let evd', rhs'' = w_coerce_to_type env evd rhs' rty evi.evar_concl in - let evd'' = solve_simple_evar_eqn env evd' ev rhs'' in + let env' = push_rels_assum (List.map (fun (_,t) -> Anonymous,t) evars') env in + let rty = Retyping.get_type_of_with_meta env' (evars_of evd) (metas_of evd) rhs' in + let evd', rhs'' = w_coerce_to_type env' evd rhs' rty evi.evar_concl in + let evd'' = solve_simple_evar_eqn env' evd' ev rhs'' in w_merge_rec evd'' metas evars' eqns end | [] -> |