diff options
| author |  pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-04-12 20:49:11 +0000 |
|---|---|---|
| committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-04-12 20:49:11 +0000 |
| commit | 3e70ea9c0967725bd320a6387d19cfb9d5a9b7fe (patch) | |
| tree | d1804bed966aefae16dff65c41a27fa0ba5a9bce /interp/constrextern.ml | |
| parent | 8d0136caf2458c2a2457550b1af1299098b1d038 (diff) | |
"A -> B" is a notation for "forall _ : A, B".
No good reason for that except uniformity so revert this commit if you find a
reason against it.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15146 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index eeb96467c..9fdf57ad9 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -194,9 +194,6 @@ let rec check_same_type ty1 ty2 = check_same_type a1 a2; check_same_type b1 b2) fl1 fl2 - | CArrow(_,a1,b1), CArrow(_,a2,b2) -> - check_same_type a1 a2; - check_same_type b1 b2 | CProdN(_,bl1,a1), CProdN(_,bl2,a2) -> List.iter2 check_same_binder bl1 bl2; check_same_type a1 a2 @@ -695,10 +692,6 @@ let rec extern inctx scopes vars r = explicitize loc inctx [] (None,sub_extern false scopes vars f) (List.map (sub_extern true scopes vars) args)) - | GProd (loc,Anonymous,_,t,c) -> - (* Anonymous product are never factorized *) - CArrow (loc,extern_typ scopes vars t, extern_typ scopes vars c) - | GLetIn (loc,na,t,c) -> CLetIn (loc,(loc,na),sub_extern false scopes vars t, extern inctx scopes (add_vname vars na) c) |