Remplacement de la dépendance de G_vernac en G_constr (source

d'incohérences dans les dépendances en l'absence de g_constr.mli) par
une dépendance en Topconstr


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9409 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 24 insertions, 20 deletions

diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index bd36002eba..da3f73149f 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -736,6 +736,24 @@ let mkLambdaC (idl,a,b) = CLambdaN (dummy_loc,[idl,a],b)
 let mkLetInC (id,a,b)   = CLetIn (dummy_loc,id,a,b)
 let mkProdC (idl,a,b)   = CProdN (dummy_loc,[idl,a],b)
 
+let rec mkCProdN loc bll c =
+  match bll with
+  | LocalRawAssum ((loc1,_)::_ as idl,t) :: bll -> 
+      CProdN (loc,[idl,t],mkCProdN (join_loc loc1 loc) bll c)
+  | LocalRawDef ((loc1,_) as id,b) :: bll -> 
+      CLetIn (loc,id,b,mkCProdN (join_loc loc1 loc) bll c)
+  | [] -> c
+  | LocalRawAssum ([],_) :: bll -> mkCProdN loc bll c
+
+let rec mkCLambdaN loc bll c =
+  match bll with
+  | LocalRawAssum ((loc1,_)::_ as idl,t) :: bll -> 
+      CLambdaN (loc,[idl,t],mkCLambdaN (join_loc loc1 loc) bll c)
+  | LocalRawDef ((loc1,_) as id,b) :: bll -> 
+      CLetIn (loc,id,b,mkCLambdaN (join_loc loc1 loc) bll c)
+  | [] -> c
+  | LocalRawAssum ([],_) :: bll -> mkCLambdaN loc bll c
+
 let rec abstract_constr_expr c = function
   | [] -> c
   | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_constr_expr c bl)
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 5ceaea67a1..7d1a7a8096 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -177,6 +177,10 @@ val coerce_to_id : constr_expr -> identifier located
 val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr
 val prod_constr_expr : constr_expr -> local_binder list -> constr_expr
 
+(* Same as [abstract_constr_expr] and [prod_constr_expr], with location *)
+val mkCLambdaN : loc -> local_binder list -> constr_expr -> constr_expr
+val mkCProdN : loc -> local_binder list -> constr_expr -> constr_expr
+
 (* For binders parsing *)
 
 (* Includes let binders *)
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 835d66434d..0f097f7e6e 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -39,24 +39,6 @@ let loc_of_binder_let = function
   | LocalRawDef ((loc,_),_)::_ -> loc
   | _ -> dummy_loc
 
-let rec mkCProdN loc bll c =
-  match bll with
-  | LocalRawAssum ((loc1,_)::_ as idl,t) :: bll -> 
-      CProdN (loc,[idl,t],mkCProdN (join_loc loc1 loc) bll c)
-  | LocalRawDef ((loc1,_) as id,b) :: bll -> 
-      CLetIn (loc,id,b,mkCProdN (join_loc loc1 loc) bll c)
-  | [] -> c
-  | LocalRawAssum ([],_) :: bll -> mkCProdN loc bll c
-
-let rec mkCLambdaN loc bll c =
-  match bll with
-  | LocalRawAssum ((loc1,_)::_ as idl,t) :: bll -> 
-      CLambdaN (loc,[idl,t],mkCLambdaN (join_loc loc1 loc) bll c)
-  | LocalRawDef ((loc1,_) as id,b) :: bll -> 
-      CLetIn (loc,id,b,mkCLambdaN (join_loc loc1 loc) bll c)
-  | [] -> c
-  | LocalRawAssum ([],_) :: bll -> mkCLambdaN loc bll c
-
 let rec index_and_rec_order_of_annot loc bl ann =
   match names_of_local_assums bl,ann with
     | [_], (None, r) -> Some 0, r
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 3684074fde..ad42304ce4 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -320,9 +320,9 @@ GEXTEND Gram
   constructor:
     [ [ id = identref; l = LIST0 binder_let; 
         coe = of_type_with_opt_coercion; c = lconstr ->
-	  (coe,(id,G_constr.mkCProdN loc l c))
+	  (coe,(id,mkCProdN loc l c))
       | id = identref; l = LIST0 binder_let ->
-	  (false,(id,G_constr.mkCProdN loc l (CHole loc))) ] ]
+	  (false,(id,mkCProdN loc l (CHole loc))) ] ]
   ;
   of_type_with_opt_coercion:
     [ [ ":>" -> true