Implemented a full-fledged equality on [constr_expr]. By the way,

some cleaning of the interface and moving of code.

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

1 files changed, 40 insertions, 14 deletions

diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index bd118bbce5..8eb88f70d8 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -17,18 +17,32 @@ open Constrexpr
 
 (** Constrexpr_ops: utilities on [constr_expr] *)
 
-val constr_loc : constr_expr -> Loc.t
+(** {6 Equalities on [constr_expr] related types} *)
 
-val cases_pattern_expr_loc : cases_pattern_expr -> Loc.t
-val raw_cases_pattern_expr_loc : raw_cases_pattern_expr -> Loc.t
+val explicitation_eq : explicitation -> explicitation -> bool
+(** Equality on [explicitation]. *)
 
-val local_binders_loc : local_binder list -> Loc.t
+val constr_expr_eq : constr_expr -> constr_expr -> bool
+(** Equality on [constr_expr]. This is a syntactical one, which is oblivious to
+    some parsing details, including locations. *)
+
+val local_binder_eq : local_binder -> local_binder -> bool
+(** Equality on [local_binder]. Same properties as [constr_expr_eq]. *)
 
 val binding_kind_eq : Decl_kinds.binding_kind -> Decl_kinds.binding_kind -> bool
+(** Equality on [binding_kind] *)
 
 val binder_kind_eq : binder_kind -> binder_kind -> bool
+(** Equality on [binder_kind] *)
 
-val default_binder_kind : binder_kind
+(** {6 Retrieving locations} *)
+
+val constr_loc : constr_expr -> Loc.t
+val cases_pattern_expr_loc : cases_pattern_expr -> Loc.t
+val raw_cases_pattern_expr_loc : raw_cases_pattern_expr -> Loc.t
+val local_binders_loc : local_binder list -> Loc.t
+
+(** {6 Constructors}*)
 
 val mkIdentC : identifier -> constr_expr
 val mkRefC : reference -> constr_expr
@@ -38,24 +52,36 @@ val mkLambdaC : name located list * binder_kind * constr_expr * constr_expr -> c
 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.t -> local_binder list -> constr_expr -> constr_expr
+(** Same as [abstract_constr_expr], with location *)
+
 val mkCProdN : Loc.t -> local_binder list -> constr_expr -> constr_expr
+(** Same as [prod_constr_expr], with location *)
 
-(** For binders parsing *)
+(** {6 Destructors}*)
 
-(** With let binders *)
-val names_of_local_assums : local_binder list -> name located list
+val coerce_reference_to_id : reference -> identifier
+(** FIXME: nothing to do here *)
+
+val coerce_to_id : constr_expr -> identifier located
+(** Destruct terms of the form [CRef (Ident _)]. *)
+
+val coerce_to_name : constr_expr -> name located
+(** Destruct terms of the form [CRef (Ident _)] or [CHole _]. *)
+
+(** {6 Binder manipulation} *)
+
+val default_binder_kind : binder_kind
 
-(** Does not take let binders into account *)
 val names_of_local_binders : local_binder list -> name located list
+(** Retrieve a list of binding names from a list of binders. *)
+
+val names_of_local_assums : local_binder list -> name located list
+(** Same as [names_of_local_binders], but does not take the [let] bindings into
+    account. *)
 
 val raw_cases_pattern_expr_of_glob_constr : (Globnames.global_reference -> unit)
   -> Glob_term.glob_constr -> raw_cases_pattern_expr