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 /pretyping/evarconv.ml | |
| 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
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 8 |
1 files changed, 4 insertions, 4 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 *) |