diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-12-06 15:04:20 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-12-06 15:04:20 +0000 |
| commit | e0099553db47314521153393b1db2cb0bdc7fbe0 (patch) | |
| tree | 89e25dd88428ae8e5abef5659797be1155f29fd9 /pretyping | |
| parent | 2e1d3dcebb35f55aa3802d034a9e2e4791a3d8c5 (diff) | |
Relâchement obligation d'une contrainte de type sur les Hole en position terminale, pour plus grande généralité de understand_gen_tcc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6421 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/pretyping.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 0054c4770..8389da9b3 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -274,10 +274,12 @@ let rec pretype tycon env isevars lvar = function anomaly "Found a pattern variable in a rawterm to type" | RHole (loc,k) -> - (match tycon with - | Some ty -> - { uj_val = e_new_evar isevars env ~src:(loc,k) ty; uj_type = ty } - | None -> error_unsolvable_implicit loc env (evars_of !isevars) k) + let ty = + match tycon with + | Some ty -> ty + | None -> + e_new_evar isevars env ~src:(loc,InternalHole) (new_Type ()) in + { uj_val = e_new_evar isevars env ~src:(loc,k) ty; uj_type = ty } | RRec (loc,fixkind,names,bl,lar,vdef) -> let rec type_bl env ctxt = function |