Basic stuff about constr_expr migrated from topconstr to constrexpr_ops

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

7 files changed, 17 insertions, 15 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 3e1af6fed7..c62039739c 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -15,6 +15,7 @@ open Term
 open Names
 open Libnames
 open Constrexpr
+open Constrexpr_ops
 open Util
 open Tok
 open Compat
@@ -32,7 +33,7 @@ let _ = List.iter Lexer.add_keyword constr_kw
 let mk_cast = function
     (c,(_,None)) -> c
   | (c,(_,Some ty)) ->
-    let loc = join_loc (Topconstr.constr_loc c) (Topconstr.constr_loc ty)
+    let loc = join_loc (constr_loc c) (constr_loc ty)
     in CCast(loc, c, CastConv ty)
 
 let binders_of_names l =
@@ -221,19 +222,19 @@ GEXTEND Gram
   ;
   record_field_declaration:
     [ [ id = global; params = LIST0 identref; ":="; c = lconstr ->
-      (id, Topconstr.abstract_constr_expr c (binders_of_lidents params)) ] ]
+      (id, abstract_constr_expr c (binders_of_lidents params)) ] ]
   ;
   binder_constr:
     [ [ forall; bl = open_binders; ","; c = operconstr LEVEL "200" ->
-          Topconstr.mkCProdN loc bl c
+          mkCProdN loc bl c
       | lambda; bl = open_binders; "=>"; c = operconstr LEVEL "200" ->
-          Topconstr.mkCLambdaN loc bl c
+          mkCLambdaN loc bl c
       | "let"; id=name; bl = binders; ty = type_cstr; ":=";
         c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" ->
           let loc1 =
-	    join_loc (Topconstr.local_binders_loc bl) (Topconstr.constr_loc c1)
+	    join_loc (local_binders_loc bl) (constr_loc c1)
 	  in
-          CLetIn(loc,id,Topconstr.mkCLambdaN loc1 bl (mk_cast(c1,ty)),c2)
+          CLetIn(loc,id,mkCLambdaN loc1 bl (mk_cast(c1,ty)),c2)
       | "let"; fx = single_fix; "in"; c = operconstr LEVEL "200" ->
           let fixp = mk_single_fix fx in
           let (li,id) = match fixp with
@@ -342,7 +343,7 @@ GEXTEND Gram
         (match p with
           | CPatAtom (_, Some r) -> CPatCstr (loc, r, lp)
           | _ -> Errors.user_err_loc
-              (Topconstr.cases_pattern_expr_loc p, "compound_pattern",
+              (cases_pattern_expr_loc p, "compound_pattern",
                Pp.str "Constructor expected."))
       |"@"; r = Prim.reference; lp = LIST1 NEXT ->
         CPatCstrExpl (loc, r, lp) ]
@@ -416,7 +417,7 @@ GEXTEND Gram
       | "("; id=name; ":="; c=lconstr; ")" ->
           [LocalRawDef (id,c)]
       | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" ->
-          [LocalRawDef (id,CCast (join_loc (Topconstr.constr_loc t) loc,c, CastConv t))]
+          [LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c, CastConv t))]
       | "{"; id=name; "}" ->
           [LocalRawAssum ([id],Default Implicit,CHole (loc, None))]
       | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" ->
diff --git a/parsing/g_obligations.ml4 b/parsing/g_obligations.ml4
index 339e0ca167..d763a1cabf 100644
--- a/parsing/g_obligations.ml4
+++ b/parsing/g_obligations.ml4
@@ -21,7 +21,7 @@ open Reduction
 open Term
 open Libnames
 open Constrexpr
-open Topconstr
+open Constrexpr_ops
 
 (* We define new entries for programs, with the use of this module
  * Subtac. These entries are named Subtac.<foo>
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index bc6571b947..927776b4ea 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -129,7 +129,7 @@ let mk_cofix_tac (loc,id,bl,ann,ty) =
 (* Functions overloaded by quotifier *)
 let induction_arg_of_constr (c,lbind as clbind) =
   if lbind = NoBindings then
-    try ElimOnIdent (Topconstr.constr_loc c,snd(Topconstr.coerce_to_id c))
+    try ElimOnIdent (Constrexpr_ops.constr_loc c,snd(Constrexpr_ops.coerce_to_id c))
     with _ -> ElimOnConstr clbind
   else ElimOnConstr clbind
 
@@ -163,8 +163,7 @@ let rec mkCLambdaN_simple_loc loc bll c =
 let mkCLambdaN_simple bl c =
   if bl=[] then c
   else
-    let loc = join_loc (fst (List.hd (pi1 (List.hd bl)))) (Topconstr
-.constr_loc c) in
+    let loc = join_loc (fst (List.hd (pi1 (List.hd bl)))) (Constrexpr_ops.constr_loc c) in
     mkCLambdaN_simple_loc loc bl c
 
 let loc_of_ne_list l = join_loc (fst (List.hd l)) (fst (list_last l))
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index f7d80a0747..3ac5b87ba1 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -13,7 +13,7 @@ open Errors
 open Util
 open Names
 open Constrexpr
-open Topconstr
+open Constrexpr_ops
 open Extend
 open Vernacexpr
 open Locality
diff --git a/parsing/grammar.mllib b/parsing/grammar.mllib
index 182234f7cf..db0c20befe 100644
--- a/parsing/grammar.mllib
+++ b/parsing/grammar.mllib
@@ -66,6 +66,7 @@ Miscops
 Glob_ops
 Detyping
 Notation_ops
+Constrexpr_ops
 Topconstr
 Genarg
 Ppextend
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 1fc7217694..f08ef361df 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -16,6 +16,7 @@ open Nameops
 open Libnames
 open Ppextend
 open Constrexpr
+open Constrexpr_ops
 open Topconstr
 open Term
 open Pattern
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 2cbc0222b4..ec164a7e34 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -23,7 +23,7 @@ open Pcoq
 open Libnames
 open Ppextend
 open Constrexpr
-open Topconstr
+open Constrexpr_ops
 open Decl_kinds
 open Tacinterp
 open Declaremods
@@ -753,7 +753,7 @@ let rec pr_vernac = function
 	++ (if redef then str" ::=" else str" :=") ++ brk(1,1) ++
 	let idl = List.map Option.get (List.filter (fun x -> not (x=None)) idl)in
         pr_raw_tactic_env
-	  (idl @ List.map Topconstr.coerce_reference_to_id
+	  (idl @ List.map coerce_reference_to_id
 	    (List.map (fun (x, _, _) -> x) (List.filter (fun (_, redef, _) -> not redef) l)))
 	  (Global.env())
 	  body in