"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

4 files changed, 0 insertions, 14 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)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 7bfe2fd78..ef3408414 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1385,8 +1385,6 @@ let internalize sigma globalenv env allow_patvar lvar c =
               Array.map (fun (bl,_,_) -> List.map snd bl) idl,
               Array.map (fun (_,ty,_) -> ty) idl,
               Array.map (fun (_,_,bd) -> bd) idl)
-    | CArrow (loc,c1,c2) ->
-        GProd (loc, Anonymous, Explicit, intern_type env c1, intern_type env c2)
     | CProdN (loc,[],c2) ->
         intern_type env c2
     | CProdN (loc,(nal,bk,ty)::bll,c2) ->
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 7d3acf66a..cbbf384a8 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -869,7 +869,6 @@ type constr_expr =
   | CRef of reference
   | CFix of loc * identifier located * fix_expr list
   | CCoFix of loc * identifier located * cofix_expr list
-  | CArrow of loc * constr_expr * constr_expr
   | CProdN of loc * (name located list * binder_kind * constr_expr) list * constr_expr
   | CLambdaN of loc * (name located list * binder_kind * constr_expr) list * constr_expr
   | CLetIn of loc * name located * constr_expr * constr_expr
@@ -955,7 +954,6 @@ let constr_loc = function
   | CRef (Qualid (loc,_)) -> loc
   | CFix (loc,_,_) -> loc
   | CCoFix (loc,_,_) -> loc
-  | CArrow (loc,_,_) -> loc
   | CProdN (loc,_,_) -> loc
   | CLambdaN (loc,_,_) -> loc
   | CLetIn (loc,_,_,_) -> loc
@@ -1053,7 +1051,6 @@ let rec fold_local_binders g f n acc b = function
       f n acc b
 
 let fold_constr_expr_with_binders g f n acc = function
-  | CArrow (loc,a,b) -> f n (f n acc a) b
   | CAppExpl (loc,(_,_),l) -> List.fold_left (f n) acc l
   | CApp (loc,(_,t),l) -> List.fold_left (f n) (f n acc t) (List.map fst l)
   | CProdN (_,l,b) | CLambdaN (_,l,b) -> fold_constr_expr_binders g f n acc b l
@@ -1207,7 +1204,6 @@ let map_local_binders f g e bl =
   (e, List.rev rbl)
 
 let map_constr_expr_with_binders g f e = function
-  | CArrow (loc,a,b) -> CArrow (loc,f e a,f e b)
   | CAppExpl (loc,r,l) -> CAppExpl (loc,r,List.map (f e) l)
   | CApp (loc,(p,a),l) ->
       CApp (loc,(p,f e a),List.map (fun (a,i) -> (f e a,i)) l)
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index b346655ad..518ae06b8 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -141,7 +141,6 @@ type constr_expr =
   | CRef of reference
   | CFix of loc * identifier located * fix_expr list
   | CCoFix of loc * identifier located * cofix_expr list
-  | CArrow of loc * constr_expr * constr_expr
   | CProdN of loc * (name located list * binder_kind * constr_expr) list * constr_expr
   | CLambdaN of loc * (name located list * binder_kind * constr_expr) list * constr_expr
   | CLetIn of loc * name located * constr_expr * constr_expr