aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/constrexpr_ops.ml142
-rw-r--r--interp/constrexpr_ops.mli53
-rw-r--r--interp/constrextern.ml1
-rw-r--r--interp/constrintern.ml1
-rw-r--r--interp/implicit_quantifiers.ml2
-rw-r--r--interp/interp.mllib1
-rw-r--r--interp/topconstr.ml120
-rw-r--r--interp/topconstr.mli35
-rw-r--r--parsing/g_constr.ml417
-rw-r--r--parsing/g_obligations.ml42
-rw-r--r--parsing/g_tactic.ml45
-rw-r--r--parsing/g_vernac.ml42
-rw-r--r--parsing/grammar.mllib1
-rw-r--r--parsing/ppconstr.ml1
-rw-r--r--parsing/ppvernac.ml4
-rw-r--r--plugins/funind/glob_term_to_relation.ml6
-rw-r--r--plugins/funind/indfun.ml32
-rw-r--r--plugins/funind/merge.ml4
-rw-r--r--tactics/extratactics.ml42
-rw-r--r--tactics/tacinterp.ml2
-rw-r--r--toplevel/command.ml1
-rw-r--r--toplevel/metasyntax.ml2
-rw-r--r--toplevel/record.ml2
23 files changed, 243 insertions, 195 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
new file mode 100644
index 000000000..18f0a38d4
--- /dev/null
+++ b/interp/constrexpr_ops.ml
@@ -0,0 +1,142 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Pp
+open Util
+open Names
+open Nameops
+open Libnames
+open Misctypes
+open Term
+open Mod_subst
+open Constrexpr
+open Decl_kinds
+
+(***********************)
+(* For binders parsing *)
+
+let default_binder_kind = Default Explicit
+
+let names_of_local_assums bl =
+ List.flatten (List.map (function LocalRawAssum(l,_,_)->l|_->[]) bl)
+
+let names_of_local_binders bl =
+ List.flatten (List.map (function LocalRawAssum(l,_,_)->l|LocalRawDef(l,_)->[l]) bl)
+
+(**********************************************************************)
+(* Functions on constr_expr *)
+
+let constr_loc = function
+ | CRef (Ident (loc,_)) -> loc
+ | CRef (Qualid (loc,_)) -> loc
+ | CFix (loc,_,_) -> loc
+ | CCoFix (loc,_,_) -> loc
+ | CProdN (loc,_,_) -> loc
+ | CLambdaN (loc,_,_) -> loc
+ | CLetIn (loc,_,_,_) -> loc
+ | CAppExpl (loc,_,_) -> loc
+ | CApp (loc,_,_) -> loc
+ | CRecord (loc,_,_) -> loc
+ | CCases (loc,_,_,_,_) -> loc
+ | CLetTuple (loc,_,_,_,_) -> loc
+ | CIf (loc,_,_,_,_) -> loc
+ | CHole (loc, _) -> loc
+ | CPatVar (loc,_) -> loc
+ | CEvar (loc,_,_) -> loc
+ | CSort (loc,_) -> loc
+ | CCast (loc,_,_) -> loc
+ | CNotation (loc,_,_) -> loc
+ | CGeneralization (loc,_,_,_) -> loc
+ | CPrim (loc,_) -> loc
+ | CDelimiters (loc,_,_) -> loc
+
+let cases_pattern_expr_loc = function
+ | CPatAlias (loc,_,_) -> loc
+ | CPatCstr (loc,_,_) -> loc
+ | CPatCstrExpl (loc,_,_) -> loc
+ | CPatAtom (loc,_) -> loc
+ | CPatOr (loc,_) -> loc
+ | CPatNotation (loc,_,_) -> loc
+ | CPatRecord (loc, _) -> loc
+ | CPatPrim (loc,_) -> loc
+ | CPatDelimiters (loc,_,_) -> loc
+
+let local_binder_loc = function
+ | LocalRawAssum ((loc,_)::_,_,t)
+ | LocalRawDef ((loc,_),t) -> join_loc loc (constr_loc t)
+ | LocalRawAssum ([],_,_) -> assert false
+
+let local_binders_loc bll =
+ if bll = [] then dummy_loc else
+ join_loc (local_binder_loc (List.hd bll)) (local_binder_loc (list_last bll))
+
+(** Pseudo-constructors *)
+
+let mkIdentC id = CRef (Ident (dummy_loc, id))
+let mkRefC r = CRef r
+let mkCastC (a,k) = CCast (dummy_loc,a,k)
+let mkLambdaC (idl,bk,a,b) = CLambdaN (dummy_loc,[idl,bk,a],b)
+let mkLetInC (id,a,b) = CLetIn (dummy_loc,id,a,b)
+let mkProdC (idl,bk,a,b) = CProdN (dummy_loc,[idl,bk,a],b)
+
+let mkAppC (f,l) =
+ let l = List.map (fun x -> (x,None)) l in
+ match f with
+ | CApp (_,g,l') -> CApp (dummy_loc, g, l' @ l)
+ | _ -> CApp (dummy_loc, (None, f), l)
+
+let rec mkCProdN loc bll c =
+ match bll with
+ | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
+ CProdN (loc,[idl,bk,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,bk,t) :: bll ->
+ CLambdaN (loc,[idl,bk,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)
+ | LocalRawAssum (idl,bk,t)::bl ->
+ List.fold_right (fun x b -> mkLambdaC([x],bk,t,b)) idl
+ (abstract_constr_expr c bl)
+
+let rec prod_constr_expr c = function
+ | [] -> c
+ | LocalRawDef (x,b)::bl -> mkLetInC(x,b,prod_constr_expr c bl)
+ | LocalRawAssum (idl,bk,t)::bl ->
+ List.fold_right (fun x b -> mkProdC([x],bk,t,b)) idl
+ (prod_constr_expr c bl)
+
+let coerce_reference_to_id = function
+ | Ident (_,id) -> id
+ | Qualid (loc,_) ->
+ Errors.user_err_loc (loc, "coerce_reference_to_id",
+ str "This expression should be a simple identifier.")
+
+let coerce_to_id = function
+ | CRef (Ident (loc,id)) -> (loc,id)
+ | a -> Errors.user_err_loc
+ (constr_loc a,"coerce_to_id",
+ str "This expression should be a simple identifier.")
+
+let coerce_to_name = function
+ | CRef (Ident (loc,id)) -> (loc,Name id)
+ | CHole (loc,_) -> (loc,Anonymous)
+ | a -> Errors.user_err_loc
+ (constr_loc a,"coerce_to_name",
+ str "This expression should be a name.")
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
new file mode 100644
index 000000000..868d53f33
--- /dev/null
+++ b/interp/constrexpr_ops.mli
@@ -0,0 +1,53 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Pp
+open Util
+open Names
+open Libnames
+open Misctypes
+open Term
+open Mod_subst
+open Constrexpr
+
+(** Constrexpr_ops: utilities on [constr_expr] *)
+
+val constr_loc : constr_expr -> loc
+
+val cases_pattern_expr_loc : cases_pattern_expr -> loc
+
+val local_binders_loc : local_binder list -> loc
+
+val default_binder_kind : binder_kind
+
+val mkIdentC : identifier -> constr_expr
+val mkRefC : reference -> constr_expr
+val mkAppC : constr_expr * constr_expr list -> constr_expr
+val mkCastC : constr_expr * constr_expr cast_type -> constr_expr
+val mkLambdaC : name located list * binder_kind * constr_expr * constr_expr -> constr_expr
+val mkLetInC : name located * constr_expr * constr_expr -> constr_expr
+val mkProdC : name located list * binder_kind * constr_expr * constr_expr -> constr_expr
+
+val coerce_reference_to_id : reference -> identifier
+val coerce_to_id : constr_expr -> identifier located
+val coerce_to_name : constr_expr -> name 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 *)
+
+(** With let binders *)
+val names_of_local_assums : local_binder list -> name located list
+
+(** Does not take let binders into account *)
+val names_of_local_binders : local_binder list -> name located list
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index c8a43c866..87a5ce73b 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -22,6 +22,7 @@ open Environ
open Libnames
open Impargs
open Constrexpr
+open Constrexpr_ops
open Notation_term
open Notation_ops
open Topconstr
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 7b5a8ebbb..480dc6ce2 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -22,6 +22,7 @@ open Patternops
open Pretyping
open Cases
open Constrexpr
+open Constrexpr_ops
open Notation_term
open Notation_ops
open Topconstr
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index a39347d55..d6e7485dc 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -246,7 +246,7 @@ let combine_params avoid fn applied needed =
aux (t' :: ids) avoid' app need
| (x,_) :: _, [] ->
- user_err_loc (Topconstr.constr_loc x,"",str "Typeclass does not expect more arguments")
+ user_err_loc (Constrexpr_ops.constr_loc x,"",str "Typeclass does not expect more arguments")
in aux [] avoid applied needed
let combine_params_freevar =
diff --git a/interp/interp.mllib b/interp/interp.mllib
index ff2549a03..ad3350f91 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -1,5 +1,6 @@
Tok
Lexer
+Constrexpr_ops
Notation_ops
Topconstr
Ppextend
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index f3bec1d0b..824b7f59a 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -20,6 +20,7 @@ open Mod_subst
open Misctypes
open Decl_kinds
open Constrexpr
+open Constrexpr_ops
open Notation_term
(*i*)
@@ -34,17 +35,6 @@ let write_oldfashion_patterns = Goptions.declare_bool_option {
Goptions.optwrite = (fun a -> oldfashion_patterns:=a);
}
-(***********************)
-(* For binders parsing *)
-
-let default_binder_kind = Default Explicit
-
-let names_of_local_assums bl =
- List.flatten (List.map (function LocalRawAssum(l,_,_)->l|_->[]) bl)
-
-let names_of_local_binders bl =
- List.flatten (List.map (function LocalRawAssum(l,_,_)->l|LocalRawDef(l,_)->[l]) bl)
-
(**********************************************************************)
(* Miscellaneous *)
@@ -54,50 +44,6 @@ let error_invalid_pattern_notation loc =
(**********************************************************************)
(* Functions on constr_expr *)
-let constr_loc = function
- | CRef (Ident (loc,_)) -> loc
- | CRef (Qualid (loc,_)) -> loc
- | CFix (loc,_,_) -> loc
- | CCoFix (loc,_,_) -> loc
- | CProdN (loc,_,_) -> loc
- | CLambdaN (loc,_,_) -> loc
- | CLetIn (loc,_,_,_) -> loc
- | CAppExpl (loc,_,_) -> loc
- | CApp (loc,_,_) -> loc
- | CRecord (loc,_,_) -> loc
- | CCases (loc,_,_,_,_) -> loc
- | CLetTuple (loc,_,_,_,_) -> loc
- | CIf (loc,_,_,_,_) -> loc
- | CHole (loc, _) -> loc
- | CPatVar (loc,_) -> loc
- | CEvar (loc,_,_) -> loc
- | CSort (loc,_) -> loc
- | CCast (loc,_,_) -> loc
- | CNotation (loc,_,_) -> loc
- | CGeneralization (loc,_,_,_) -> loc
- | CPrim (loc,_) -> loc
- | CDelimiters (loc,_,_) -> loc
-
-let cases_pattern_expr_loc = function
- | CPatAlias (loc,_,_) -> loc
- | CPatCstr (loc,_,_) -> loc
- | CPatCstrExpl (loc,_,_) -> loc
- | CPatAtom (loc,_) -> loc
- | CPatOr (loc,_) -> loc
- | CPatNotation (loc,_,_) -> loc
- | CPatRecord (loc, _) -> loc
- | CPatPrim (loc,_) -> loc
- | CPatDelimiters (loc,_,_) -> loc
-
-let local_binder_loc = function
- | LocalRawAssum ((loc,_)::_,_,t)
- | LocalRawDef ((loc,_),t) -> join_loc loc (constr_loc t)
- | LocalRawAssum ([],_,_) -> assert false
-
-let local_binders_loc bll =
- if bll = [] then dummy_loc else
- join_loc (local_binder_loc (List.hd bll)) (local_binder_loc (list_last bll))
-
let ids_of_cases_indtype =
let rec vars_of ids = function
(* We deal only with the regular cases *)
@@ -202,70 +148,6 @@ let free_vars_of_constr_expr c =
let occur_var_constr_expr id c = Idset.mem id (free_vars_of_constr_expr c)
-let mkIdentC id = CRef (Ident (dummy_loc, id))
-let mkRefC r = CRef r
-let mkCastC (a,k) = CCast (dummy_loc,a,k)
-let mkLambdaC (idl,bk,a,b) = CLambdaN (dummy_loc,[idl,bk,a],b)
-let mkLetInC (id,a,b) = CLetIn (dummy_loc,id,a,b)
-let mkProdC (idl,bk,a,b) = CProdN (dummy_loc,[idl,bk,a],b)
-
-let mkAppC (f,l) =
- let l = List.map (fun x -> (x,None)) l in
- match f with
- | CApp (_,g,l') -> CApp (dummy_loc, g, l' @ l)
- | _ -> CApp (dummy_loc, (None, f), l)
-
-let rec mkCProdN loc bll c =
- match bll with
- | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
- CProdN (loc,[idl,bk,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,bk,t) :: bll ->
- CLambdaN (loc,[idl,bk,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)
- | LocalRawAssum (idl,bk,t)::bl ->
- List.fold_right (fun x b -> mkLambdaC([x],bk,t,b)) idl
- (abstract_constr_expr c bl)
-
-let rec prod_constr_expr c = function
- | [] -> c
- | LocalRawDef (x,b)::bl -> mkLetInC(x,b,prod_constr_expr c bl)
- | LocalRawAssum (idl,bk,t)::bl ->
- List.fold_right (fun x b -> mkProdC([x],bk,t,b)) idl
- (prod_constr_expr c bl)
-
-let coerce_reference_to_id = function
- | Ident (_,id) -> id
- | Qualid (loc,_) ->
- user_err_loc (loc, "coerce_reference_to_id",
- str "This expression should be a simple identifier.")
-
-let coerce_to_id = function
- | CRef (Ident (loc,id)) -> (loc,id)
- | a -> user_err_loc
- (constr_loc a,"coerce_to_id",
- str "This expression should be a simple identifier.")
-
-let coerce_to_name = function
- | CRef (Ident (loc,id)) -> (loc,Name id)
- | CHole (loc,_) -> (loc,Anonymous)
- | a -> user_err_loc
- (constr_loc a,"coerce_to_name",
- str "This expression should be a name.")
-
(* Interpret the index of a recursion order annotation *)
let split_at_annot bl na =
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 7556f1385..482d409ba 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -24,52 +24,17 @@ val oldfashion_patterns : bool ref
(** Utilities on constr_expr *)
-val constr_loc : constr_expr -> loc
-
-val cases_pattern_expr_loc : cases_pattern_expr -> loc
-
-val local_binders_loc : local_binder list -> loc
-
val replace_vars_constr_expr :
(identifier * identifier) list -> constr_expr -> constr_expr
val free_vars_of_constr_expr : constr_expr -> Idset.t
val occur_var_constr_expr : identifier -> constr_expr -> bool
-val default_binder_kind : binder_kind
-
(** Specific function for interning "in indtype" syntax of "match" *)
val ids_of_cases_indtype : cases_pattern_expr -> identifier list
-val mkIdentC : identifier -> constr_expr
-val mkRefC : reference -> constr_expr
-val mkAppC : constr_expr * constr_expr list -> constr_expr
-val mkCastC : constr_expr * constr_expr cast_type -> constr_expr
-val mkLambdaC : name located list * binder_kind * constr_expr * constr_expr -> constr_expr
-val mkLetInC : name located * constr_expr * constr_expr -> constr_expr
-val mkProdC : name located list * binder_kind * constr_expr * constr_expr -> constr_expr
-
-val coerce_reference_to_id : reference -> identifier
-val coerce_to_id : constr_expr -> identifier located
-val coerce_to_name : constr_expr -> name located
-
val split_at_annot : local_binder list -> identifier located option -> local_binder list * local_binder list
-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 *)
-
-(** With let binders *)
-val names_of_local_binders : local_binder list -> name located list
-
-(** Does not take let binders into account *)
-val names_of_local_assums : local_binder list -> name located list
-
(** Used in typeclasses *)
val fold_constr_expr_with_binders : (identifier -> 'a -> 'a) ->
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 3e1af6fed..c62039739 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 339e0ca16..d763a1cab 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 bc6571b94..927776b4e 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 f7d80a074..3ac5b87ba 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 182234f7c..db0c20bef 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 1fc721769..f08ef361d 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 2cbc0222b..ec164a7e3 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
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 9fe77bf9d..cf9b54a94 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1307,7 +1307,7 @@ let do_build_inductive
else
Constrexpr.CProdN
(dummy_loc,
- [[(dummy_loc,n)],Topconstr.default_binder_kind,Constrextern.extern_glob_constr Idset.empty t],
+ [[(dummy_loc,n)],Constrexpr_ops.default_binder_kind,Constrextern.extern_glob_constr Idset.empty t],
acc
)
)
@@ -1373,7 +1373,7 @@ let do_build_inductive
else
Constrexpr.CProdN
(dummy_loc,
- [[(dummy_loc,n)],Topconstr.default_binder_kind,Constrextern.extern_glob_constr Idset.empty t],
+ [[(dummy_loc,n)],Constrexpr_ops.default_binder_kind,Constrextern.extern_glob_constr Idset.empty t],
acc
)
)
@@ -1393,7 +1393,7 @@ let do_build_inductive
Constrexpr.LocalRawDef((dummy_loc,n), Constrextern.extern_glob_constr Idset.empty t)
else
Constrexpr.LocalRawAssum
- ([(dummy_loc,n)], Topconstr.default_binder_kind, Constrextern.extern_glob_constr Idset.empty t)
+ ([(dummy_loc,n)], Constrexpr_ops.default_binder_kind, Constrextern.extern_glob_constr Idset.empty t)
)
rels_params
in
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 2eb2fb3ed..d3f56341f 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -130,9 +130,9 @@ let functional_induction with_clean c princl pat =
let rec abstract_glob_constr c = function
| [] -> c
- | Constrexpr.LocalRawDef (x,b)::bl -> Topconstr.mkLetInC(x,b,abstract_glob_constr c bl)
+ | Constrexpr.LocalRawDef (x,b)::bl -> Constrexpr_ops.mkLetInC(x,b,abstract_glob_constr c bl)
| Constrexpr.LocalRawAssum (idl,k,t)::bl ->
- List.fold_right (fun x b -> Topconstr.mkLambdaC([x],k,t,b)) idl
+ List.fold_right (fun x b -> Constrexpr_ops.mkLambdaC([x],k,t,b)) idl
(abstract_glob_constr c bl)
let interp_casted_constr_with_implicits sigma env impls c =
@@ -152,7 +152,7 @@ let build_newrecursive
let (rec_sign,rec_impls) =
List.fold_left
(fun (env,impls) ((_,recname),bl,arityc,_) ->
- let arityc = Topconstr.prod_constr_expr arityc bl in
+ let arityc = Constrexpr_ops.prod_constr_expr arityc bl in
let arity = Constrintern.interp_type sigma env0 arityc in
let impl = Constrintern.compute_internalization_data env0 Constrintern.Recursive arity [] in
(Environ.push_named (recname,None,arity) env, Idmap.add recname impl impls))
@@ -379,12 +379,12 @@ let generate_correction_proof_wf f_ref tcc_lemma_ref
let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas args ret_type body
pre_hook
=
- let type_of_f = Topconstr.prod_constr_expr ret_type args in
+ let type_of_f = Constrexpr_ops.prod_constr_expr ret_type args in
let rec_arg_num =
let names =
List.map
snd
- (Topconstr.names_of_local_assums args)
+ (Constrexpr_ops.names_of_local_assums args)
in
match wf_arg with
| None ->
@@ -401,16 +401,16 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
(List.map
(function
| _,Anonymous -> assert false
- | _,Name e -> (Topconstr.mkIdentC e)
+ | _,Name e -> (Constrexpr_ops.mkIdentC e)
)
- (Topconstr.names_of_local_assums args)
+ (Constrexpr_ops.names_of_local_assums args)
)
)
in
- Constrexpr.CApp (dummy_loc,(None,Topconstr.mkRefC (Qualid (dummy_loc,(qualid_of_string "Logic.eq")))),
+ Constrexpr.CApp (dummy_loc,(None,Constrexpr_ops.mkRefC (Qualid (dummy_loc,(qualid_of_string "Logic.eq")))),
[(f_app_args,None);(body,None)])
in
- let eq = Topconstr.prod_constr_expr unbounded_eq args in
+ let eq = Constrexpr_ops.prod_constr_expr unbounded_eq args in
let hook f_ref tcc_lemma_ref functional_ref eq_ref rec_arg_num rec_arg_type
nb_args relation =
try
@@ -469,25 +469,25 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
in
let fun_from_mes =
let applied_mes =
- Topconstr.mkAppC(wf_mes_expr,[Topconstr.mkIdentC wf_arg]) in
- Topconstr.mkLambdaC ([(dummy_loc,Name wf_arg)],Topconstr.default_binder_kind,wf_arg_type,applied_mes)
+ Constrexpr_ops.mkAppC(wf_mes_expr,[Constrexpr_ops.mkIdentC wf_arg]) in
+ Constrexpr_ops.mkLambdaC ([(dummy_loc,Name wf_arg)],Constrexpr_ops.default_binder_kind,wf_arg_type,applied_mes)
in
let wf_rel_from_mes =
- Topconstr.mkAppC(Topconstr.mkRefC ltof,[wf_arg_type;fun_from_mes])
+ Constrexpr_ops.mkAppC(Constrexpr_ops.mkRefC ltof,[wf_arg_type;fun_from_mes])
in
wf_rel_from_mes,true
| Some wf_rel_expr ->
let wf_rel_with_mes =
let a = Names.id_of_string "___a" in
let b = Names.id_of_string "___b" in
- Topconstr.mkLambdaC(
+ Constrexpr_ops.mkLambdaC(
[dummy_loc,Name a;dummy_loc,Name b],
Constrexpr.Default Explicit,
wf_arg_type,
- Topconstr.mkAppC(wf_rel_expr,
+ Constrexpr_ops.mkAppC(wf_rel_expr,
[
- Topconstr.mkAppC(wf_mes_expr,[Topconstr.mkIdentC a]);
- Topconstr.mkAppC(wf_mes_expr,[Topconstr.mkIdentC b])
+ Constrexpr_ops.mkAppC(wf_mes_expr,[Constrexpr_ops.mkIdentC a]);
+ Constrexpr_ops.mkAppC(wf_mes_expr,[Constrexpr_ops.mkIdentC b])
])
)
in
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 4ca23a295..ebe5cebd2 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -830,7 +830,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
let _ = prNamedRConstr (string_of_name nme) tp in
let _ = prstr " ; " in
let typ = glob_constr_to_constr_expr tp in
- LocalRawAssum ([(dummy_loc,nme)], Topconstr.default_binder_kind, typ) :: acc)
+ LocalRawAssum ([(dummy_loc,nme)], Constrexpr_ops.default_binder_kind, typ) :: acc)
[] params in
let concl = Constrextern.extern_constr false (Global.env()) concl in
let arity,_ =
@@ -838,7 +838,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
(fun (acc,env) (nm,_,c) ->
let typ = Constrextern.extern_constr false env c in
let newenv = Environ.push_rel (nm,None,c) env in
- CProdN (dummy_loc, [[(dummy_loc,nm)],Topconstr.default_binder_kind,typ] , acc) , newenv)
+ CProdN (dummy_loc, [[(dummy_loc,nm)],Constrexpr_ops.default_binder_kind,typ] , acc) , newenv)
(concl,Global.env())
(shift.funresprms2 @ shift.funresprms1
@ shift.args2 @ shift.args1 @ shift.otherprms2 @ shift.otherprms1) in
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index a74bdad29..db55f6434 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -250,7 +250,7 @@ TACTIC EXTEND rewrite_star
let add_rewrite_hint name ort t lcsr =
let env = Global.env() and sigma = Evd.empty in
- let f c = Topconstr.constr_loc c, Constrintern.interp_constr sigma env c, ort, t in
+ let f c = Constrexpr_ops.constr_loc c, Constrintern.interp_constr sigma env c, ort, t in
add_rew_rules name (List.map f lcsr)
VERNAC COMMAND EXTEND HintRewrite
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 462ffdc38..a0fd61c06 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -34,7 +34,7 @@ open Refiner
open Tacmach
open Tactic_debug
open Constrexpr
-open Topconstr
+open Constrexpr_ops
open Term
open Termops
open Tacexpr
diff --git a/toplevel/command.ml b/toplevel/command.ml
index a1d6eecf2..0cf5aaa68 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -20,6 +20,7 @@ open Names
open Libnames
open Nameops
open Constrexpr
+open Constrexpr_ops
open Topconstr
open Constrintern
open Nametab
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 6b64f9546..203d8ba02 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -13,9 +13,9 @@ open Errors
open Util
open Names
open Constrexpr
+open Constrexpr_ops
open Notation_term
open Notation_ops
-open Topconstr
open Ppextend
open Extend
open Libobject
diff --git a/toplevel/record.ml b/toplevel/record.ml
index f4ef35e01..84592f2a7 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -26,7 +26,7 @@ open Decl_kinds
open Indtypes
open Type_errors
open Constrexpr
-open Topconstr
+open Constrexpr_ops
(********** definition d'un record (structure) **************)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 21:42:10 +0000