diff options
| author | herbelin | 2011-10-25 14:04:10 +0000 |
|---|---|---|
| committer | herbelin | 2011-10-25 14:04:10 +0000 |
| commit | 73608dad07000dddead80ba223729c824b8bb2c2 (patch) | |
| tree | 392b4575f622c06c5a476dab54303e30421a5612 | |
| parent | ad3833f141d0ac42d5590c30cf1c128418493d4c (diff) | |
Fixing use of type constraint for refining the "return" clause of "match".
Adams Chlipala's ltamer now compatible with forthcoming 8.4; thanks to
Matthieu for how to reactivate inh_conv_coerces_to.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14596 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/cases.ml | 10 | ||||
| -rw-r--r-- | pretyping/coercion.ml | 9 |
2 files changed, 14 insertions, 5 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 6559084578..163d37f964 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1655,13 +1655,15 @@ let prepare_predicate loc typing_fun sigma env tomatchs sign tycon pred = (* Some type annotation *) | Some rtntyp, _ -> (* We extract the signature of the arity *) - let env = List.fold_right push_rels arsign env in + let envar = List.fold_right push_rels arsign env in let sigma, newt = new_sort_variable sigma in let evdref = ref sigma in - let predcclj = typing_fun (mk_tycon (mkSort newt)) env evdref rtntyp in + let predcclj = typing_fun (mk_tycon (mkSort newt)) envar evdref rtntyp in let sigma = Option.cata (fun tycon -> - let tycon = lift_tycon_type (List.length arsign) tycon in - Coercion.inh_conv_coerces_to loc env !evdref predcclj.uj_val tycon) + let na = (Name (id_of_string "x"),KnownNotDep) in + let tms = List.map (fun tm -> Pushed(tm,[],na)) tomatchs in + let predinst = extract_predicate [] predcclj.uj_val tms in + Coercion.inh_conv_coerces_to loc env !evdref predinst tycon) !evdref tycon in let predccl = (j_nf_evar sigma predcclj).uj_val in [sigma, KnownDep, predccl] diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 389761aeb9..553c912747 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -242,7 +242,14 @@ module Default = struct let inh_conv_coerce_rigid_to = inh_conv_coerce_to_gen true - let inh_conv_coerces_to loc env (evd : evar_map) t (abs, t') = evd + let inh_conv_coerces_to loc env (evd : evar_map) t (abs, t') = + if abs = None then + try + fst (inh_conv_coerce_to_fail loc env evd true None t t') + with NoCoercion -> + evd (* Maybe not enough information to unify *) + else + evd (* Still problematic, as it changes unification let nabsinit, nabs = match abs with |