diff options
| author | msozeau | 2008-11-07 14:05:05 +0000 |
|---|---|---|
| committer | msozeau | 2008-11-07 14:05:05 +0000 |
| commit | 6d7cd9583e50c60c5dfa076f4f8a3b8add37a755 (patch) | |
| tree | 20b2cee2ddee4fc60ef37af1ef9c4757a5612357 | |
| parent | b626be96132d2dc65be5acb054d343a9eeffc826 (diff) | |
Fix universe problem appearing ConCaT using the existing infrastructure for
declaring additional conversion problems when unifying the type of an
evar instance and the evar's declared type. Fix the corresponding
conversion heuristic which failed due to (misplaced?) assertions when
faced with general conversion problems.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11549 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/evarconv.ml | 8 | ||||
| -rw-r--r-- | pretyping/evarutil.ml | 2 |
2 files changed, 5 insertions, 5 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 667ea458cc..c682829087 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -514,15 +514,15 @@ let apply_conversion_problem_heuristic env evd pbty t1 t2 = let (term1,l1 as appr1) = decompose_app t1 in let (term2,l2 as appr2) = decompose_app t2 in match kind_of_term term1, kind_of_term term2 with - | Evar (evk1,args1), (Rel _|Var _) when l1 = [] & l2 = [] -> + | Evar (evk1,args1), (Rel _|Var _) when l1 = [] & l2 = [] + & array_for_all (fun a -> a = term2 or isEvar a) args1 -> (* The typical kind of constraint coming from pattern-matching return type inference *) - assert (array_for_all (fun a -> a = term2 or isEvar a) args1); choose_less_dependent_instance evk1 evd term2 args1, true - | (Rel _|Var _), Evar (evk2,args2) when l1 = [] & l2 = [] -> + | (Rel _|Var _), Evar (evk2,args2) when l1 = [] & l2 = [] + & array_for_all (fun a -> a = term1 or isEvar a) args2 -> (* The typical kind of constraint coming from pattern-matching return type inference *) - assert (array_for_all ((=) term1) args2); choose_less_dependent_instance evk2 evd term1 args2, true | Evar ev1,_ when List.length l1 <= List.length l2 -> (* On "?n t1 .. tn = u u1 .. u(n+p)", try first-order unification *) diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index aed50c4687..fafdfe9950 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -1059,7 +1059,7 @@ let solve_simple_eqn conv_algo env evd (pbty,(evk1,args1 as ev1),t2) = let evc = nf_isevar evd evi.evar_concl in let body = match evi.evar_body with Evar_defined b -> b | Evar_empty -> assert false in let ty = nf_isevar evd (Retyping.get_type_of_with_meta evenv evm (metas_of evd) body) in - fst (conv_algo evenv evd Reduction.CUMUL ty evc) + add_conv_pb (Reduction.CUMUL,evenv,ty,evc) evd else evd in let (evd,pbs) = extract_changed_conv_pbs evd status_changed in |