"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

13 files changed, 28 insertions, 67 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index eeb96467c3..9fdf57ad9f 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 7bfe2fd78e..ef3408414c 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 7d3acf66a8..cbbf384a89 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 b346655ad7..518ae06b8f 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
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index f60d06857d..abd1607d67 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -170,9 +170,7 @@ GEXTEND Gram
       | c1 = operconstr; ":>" ->
                  CCast(loc,c1, CastCoerce) ]
     | "99" RIGHTA [ ]
-    | "90" RIGHTA
-      [ c1 = operconstr; "->"; c2 = binder_constr -> CArrow(loc,c1,c2)
-      | c1 = operconstr; "->"; c2 = SELF -> CArrow(loc,c1,c2)]
+    | "90" RIGHTA [ ]
     | "10" LEFTA
       [ f=operconstr; args=LIST1 appl_arg -> CApp(loc,(None,f),args)
       | "@"; f=global; args=LIST0 NEXT -> CAppExpl(loc,(None,f),args)
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 20479fe148..98ed6883e2 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -309,7 +309,6 @@ let rename na na' t c =
     | _ -> (na',t,c)
 
 let split_product na' = function
-  | CArrow (loc,t,c) -> (na',t,c)
   | CProdN (loc,[[na],bk,t],c) -> rename na na' t c
   | CProdN (loc,([na],bk,t)::bl,c) -> rename na na' t (CProdN(loc,bl,c))
   | CProdN (loc,(na::nal,bk,t)::bl,c) ->
@@ -428,10 +427,6 @@ let pr pr sep inherited a =
              pr_recursive
               (pr_cofixdecl (pr mt) (pr_dangling_with_for mt pr)) (snd id) cofix),
       lfix
-  | CArrow (_,a,b) ->
-      hov 0 (pr mt (larrow,L) a ++ str " ->" ++
-             pr (fun () ->brk(1,0)) (-larrow,E) b),
-      larrow
   | CProdN _ ->
       let (bl,a) = extract_prod_binders a in
       hov 0 (
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 1e0f2aef2a..c4c8579d95 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -296,10 +296,6 @@ let strip_prod_binders_expr n ty =
 	  let bll = List.map (fun (x, _, y) -> x, y) bll in
             if nb >= n then (List.rev (bll@acc)), a
             else strip_ty (bll@acc) (n-nb) a
-      | Topconstr.CArrow(_,a,b) ->
-          if n=1 then
-            (List.rev (([(dummy_loc,Anonymous)],a)::acc), b)
-          else strip_ty (([(dummy_loc,Anonymous)],a)::acc) (n-1) b
       | _ -> error "Cannot translate fix tactic: not enough products" in
   strip_ty [] n ty
 
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index df25972082..f364652077 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -135,8 +135,6 @@ let rec mlexpr_of_constr = function
   | Topconstr.CRef r -> <:expr< Topconstr.CRef $mlexpr_of_reference r$ >>
   | Topconstr.CFix (loc,_,_) -> failwith "mlexpr_of_constr: TODO"
   | Topconstr.CCoFix (loc,_,_) -> failwith "mlexpr_of_constr: TODO"
-  | Topconstr.CArrow (loc,a,b) ->
-  <:expr< Topconstr.CArrow $dloc$ $mlexpr_of_constr a$ $mlexpr_of_constr b$ >>
   | Topconstr.CProdN (loc,l,a) -> <:expr< Topconstr.CProdN $dloc$ $mlexpr_of_list
       (mlexpr_of_triple (mlexpr_of_list (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_name)) mlexpr_of_binder_kind mlexpr_of_constr) l$ $mlexpr_of_constr a$ >>
   | Topconstr.CLambdaN (loc,l,a) -> <:expr< Topconstr.CLambdaN $dloc$ $mlexpr_of_list (mlexpr_of_triple (mlexpr_of_list (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_name)) mlexpr_of_binder_kind mlexpr_of_constr) l$ $mlexpr_of_constr a$ >>
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index a7298095ea..954e389a4e 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1256,11 +1256,10 @@ let rec rebuild_return_type rt =
   match rt with
     | Topconstr.CProdN(loc,n,t') ->
 	Topconstr.CProdN(loc,n,rebuild_return_type t')
-    | Topconstr.CArrow(loc,t,t') ->
-	Topconstr.CArrow(loc,t,rebuild_return_type t')
     | Topconstr.CLetIn(loc,na,t,t') ->
 	Topconstr.CLetIn(loc,na,t,rebuild_return_type t')
-    | _ -> Topconstr.CArrow(dummy_loc,rt,Topconstr.CSort(dummy_loc,GType None))
+    | _ -> Topconstr.CProdN(dummy_loc,[[dummy_loc,Names.Anonymous],Topconstr.Default Glob_term.Explicit,rt],
+			    Topconstr.CSort(dummy_loc,GType None))
 
 
 let do_build_inductive
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 31814b141e..42df294a05 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -549,14 +549,6 @@ let decompose_prod_n_assum_constr_expr =
 	  (List.rev (Topconstr.LocalRawAssum(nal_keep,bk,nal_type)::acc),
 	   Topconstr.CLambdaN(lambda_loc,(nal_expr,bk,nal_type)::bl,e')
 	  )
-      | Topconstr.CArrow(_,premisse,concl) -> 
-	(* let _ = Pp.msgnl (str "arrow case") in  *)
-	decompose_prod_n_assum_constr_expr 
-	  (Topconstr.LocalRawAssum([dummy_loc,Names.Anonymous],
-				   Topconstr.Default Lib.Explicit,premisse)
-	  ::acc)
-	  (pred n)
-	  concl
       | Topconstr.CLetIn(_, na,nav,e') -> 
 	decompose_prod_n_assum_constr_expr 
 	  (Topconstr.LocalRawDef(na,nav)::acc) (pred n) e'
@@ -565,12 +557,14 @@ let decompose_prod_n_assum_constr_expr =
   decompose_prod_n_assum_constr_expr []
 
 open Topconstr
-    
-let id_of_name = function 
-  | Name id -> id 
-  | _ -> assert false
 
- let rec rebuild_bl (aux,assoc) bl typ = 
+let rec make_assoc = List.fold_left2 (fun l a b ->
+match a, b with
+  |(_,Name na), (_, Name id) -> (na, id)::l
+  |_,_ -> l
+)
+
+let rec rebuild_bl (aux,assoc) bl typ = 
 	match bl,typ with 
 	  | [], _ -> (List.rev aux,replace_vars_constr_expr assoc typ,assoc)
 	  | (Topconstr.LocalRawAssum(nal,bk,_))::bl',typ -> 
@@ -582,17 +576,13 @@ let id_of_name = function
       and rebuild_nal (aux,assoc) bk bl' nal lnal typ = 
 	match nal,typ with 
 	  | [], _ -> rebuild_bl (aux,assoc) bl' typ
-	  | na::nal,CArrow(_,nat,typ') -> 
-	    rebuild_nal 
-	      ((LocalRawAssum([na],bk,replace_vars_constr_expr assoc nat))::aux,assoc) 
-	      bk bl' nal (pred lnal) typ'
 	  | _,CProdN(_,[],typ) -> rebuild_nal (aux,assoc) bk bl' nal lnal typ
 	  | _,CProdN(_,(nal',bk',nal't)::rest,typ') -> 
 	    let lnal' = List.length nal' in 
 	    if lnal' >= lnal 
 	    then 
 	      let old_nal',new_nal' = list_chop lnal nal' in 
-	      rebuild_bl ((LocalRawAssum(nal,bk,replace_vars_constr_expr assoc nal't)::aux),(List.rev_append (List.combine (List.map id_of_name (List.map snd old_nal'))  (List.map id_of_name (List.map snd nal))) assoc)) bl' 
+	      rebuild_bl ((LocalRawAssum(nal,bk,replace_vars_constr_expr assoc nal't)::aux),(make_assoc assoc old_nal' nal)) bl' 
 		(if new_nal' = [] && rest = []
 		 then  typ' 
 		 else if new_nal' = [] 
@@ -600,7 +590,7 @@ let id_of_name = function
 		 else CProdN(dummy_loc,((new_nal',bk',nal't)::rest),typ'))
 	    else 
 	      let captured_nal,non_captured_nal = list_chop lnal' nal in 
-	      rebuild_nal ((LocalRawAssum(captured_nal,bk,replace_vars_constr_expr assoc nal't)::aux), (List.rev_append (List.combine (List.map id_of_name (List.map snd captured_nal)) ((List.map id_of_name (List.map snd nal)))) assoc))
+	      rebuild_nal ((LocalRawAssum(captured_nal,bk,replace_vars_constr_expr assoc nal't)::aux), (make_assoc assoc nal' captured_nal))
 		bk bl' non_captured_nal (lnal - lnal') (CProdN(dummy_loc,rest,typ'))
 	  | _ -> assert false
 
@@ -711,8 +701,6 @@ let rec add_args id new_args b =
 	| _ -> b
       end
   | CFix  _  | CCoFix _ -> anomaly "add_args : todo"
-  | CArrow(loc,b1,b2) ->
-      CArrow(loc,add_args id new_args  b1, add_args id new_args b2)
   | CProdN(loc,nal,b1) ->
       CProdN(loc,
 	     List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal,
@@ -779,8 +767,6 @@ let rec chop_n_arrow n t =
   then t (* If we have already removed all the arrows then return the type *)
   else (* If not we check the form of [t] *)
     match t with
-      | Topconstr.CArrow(_,_,t) ->  (* If we have an arrow, we discard it and recall [chop_n_arrow] *)
-	  chop_n_arrow (n-1) t
       | Topconstr.CProdN(_,nal_ta',t') -> (* If we have a forall, to result are possible :
 					     either we need to discard more than the number of arrows contained
 					     in this product declaration then we just recall [chop_n_arrow] on
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index c953bedcba..036c4f0ea8 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -172,10 +172,10 @@ let flatten_contravariant_disj ist =
 let not_dep_intros ist =
   <:tactic<
   repeat match goal with
-  | |- (?X1 -> ?X2) => intro
+  | |- (forall (_: ?X1), ?X2) => intro
   | |- (Coq.Init.Logic.not _)   => unfold Coq.Init.Logic.not at 1
   | H:(Coq.Init.Logic.not _)|-_    => unfold Coq.Init.Logic.not at 1 in H
-  | H:(Coq.Init.Logic.not _)->_|-_    => unfold Coq.Init.Logic.not at 1 in H
+  | H:forall (_: Coq.Init.Logic.not _), _|-_    => unfold Coq.Init.Logic.not at 1 in H
   end >>
 
 let axioms ist =
@@ -204,25 +204,25 @@ let simplif ist =
         | id: (Coq.Init.Logic.iff _ _) |- _ => elim id; do 2 intro; clear id
         | id: (Coq.Init.Logic.not _) |- _ => red in id
         | id: ?X1 |- _ => $t_is_disj; elim id; intro; clear id
-        | id0: ?X1 -> ?X2, id1: ?X1|- _ =>
+        | id0: (forall (_: ?X1), ?X2), id1: ?X1|- _ =>
 	    (* generalize (id0 id1); intro; clear id0 does not work
 	       (see Marco Maggiesi's bug PR#301)
 	    so we instead use Assert and exact. *)
 	    assert X2; [exact (id0 id1) | clear id0]
-        | id: ?X1 -> ?X2|- _ =>
+        | id: forall (_ : ?X1), ?X2|- _ =>
           $t_is_unit_or_eq; cut X2;
 	    [ intro; clear id
-	    | (* id : ?X1 -> ?X2 |- ?X2 *)
+	    | (* id : forall (_: ?X1), ?X2 |- ?X2 *)
 	      cut X1; [exact id| constructor 1; fail]
 	    ]
-        | id: ?X1 -> ?X2|- _ =>
+        | id: forall (_ : ?X1), ?X2|- _ =>
           $t_flatten_contravariant_conj
 	  (* moved from "id:(?A/\?B)->?X2|-" to "?A->?B->?X2|-" *)
-        | id: (Coq.Init.Logic.iff ?X1 ?X2) -> ?X3|- _ =>
-          assert ((X1 -> X2) -> (X2 -> X1) -> X3)
+        | id: forall (_: Coq.Init.Logic.iff ?X1 ?X2), ?X3|- _ =>
+          assert (forall (_: forall _:X1, X2), forall (_: forall _: X2, X1), X3)
 	    by (do 2 intro; apply id; split; assumption);
             clear id
-        | id: ?X1 -> ?X2|- _ =>
+        | id: forall (_:?X1), ?X2|- _ =>
           $t_flatten_contravariant_disj
 	  (* moved from "id:(?A\/?B)->?X2|-" to "?A->?X2,?B->?X2|-" *)
         | |- ?X1 => $t_is_conj; split
@@ -240,10 +240,10 @@ let rec tauto_intuit t_reduce solver ist =
   <:tactic<
    ($t_simplif;$t_axioms
    || match reverse goal with
-      | id:(?X1 -> ?X2)-> ?X3|- _ =>
+      | id:forall(_: forall (_: ?X1), ?X2), ?X3|- _ =>
 	  cut X3;
 	    [ intro; clear id; $t_tauto_intuit
-	    | cut (X1 -> X2);
+	    | cut (forall (_: X1), X2);
 		[ exact id
 		| generalize (fun y:X2 => id (fun x:X1 => y)); intro; clear id;
 		  solve [ $t_tauto_intuit ]]]
@@ -252,7 +252,7 @@ let rec tauto_intuit t_reduce solver ist =
       end
     ||
     (* NB: [|- _ -> _] matches any product *)
-    match goal with | |- _ -> _ => intro; $t_tauto_intuit
+    match goal with | |- forall (_ : _),  _ => intro; $t_tauto_intuit
     |  |- _  => $t_reduce;$t_solver
     end
     ||
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index ca7d0073e1..d391611dc2 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -8,7 +8,9 @@
 
 Set Implicit Arguments.
 
-Require Import Notations.
+Require Export Notations.
+
+Notation "A -> B" := (forall (_ : A), B) : type_scope.
 
 (** * Propositional connectives *)
 
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index 490cbf5736..1171fcca25 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -10,6 +10,7 @@
 
 (** Notations for propositional connectives *)
 
+Reserved Notation "x -> y" (at level 90, right associativity, y at level 200).
 Reserved Notation "x <-> y" (at level 95, no associativity).
 Reserved Notation "x /\ y" (at level 80, right associativity).
 Reserved Notation "x \/ y" (at level 85, right associativity).