mli comments for doc

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

2 files changed, 22 insertions, 25 deletions

diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 35932bb8e..d3a2452de 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -15,10 +15,9 @@ open Evd
 open Environ
 open Reductionops
 
-(** {6 This modules provides useful functions for unification modulo evars } *)
+(** {5 This modules provides useful functions for unification modulo evars } *)
 
-(**********************************************************
-   Metas *)
+(** {6 Metas} *)
 
 (** [new_meta] is a generator of unique meta variables *)
 val new_meta : unit -> metavariable
@@ -27,8 +26,7 @@ val mk_new_meta : unit -> constr
 (** [new_untyped_evar] is a generator of unique evar keys *)
 val new_untyped_evar : unit -> existential_key
 
-(**********************************************************
-   Creating a fresh evar given their type and context *)
+(** {6 Creating a fresh evar given their type and context} *)
 val new_evar :
   evar_map -> env -> ?src:loc * hole_kind -> ?filter:bool list -> types -> evar_map * constr
 
@@ -47,8 +45,7 @@ val new_evar_instance :
 
 val make_pure_subst : evar_info -> constr array -> (identifier * constr) list
 
-(**********************************************************
-   Instantiate evars *)
+(** {6 Instantiate evars} *)
 
 (** [evar_define choose env ev c] try to instantiate [ev] with [c] (typed in [env]),
    possibly solving related unification problems, possibly leaving open
@@ -56,8 +53,7 @@ val make_pure_subst : evar_info -> constr array -> (identifier * constr) list
    true); fails if the instance is not valid for the given [ev] *)
 val evar_define : ?choose:bool -> env -> existential -> constr -> evar_map -> evar_map
 
-(**********************************************************
-   Evars/Metas switching... *)
+(** {6 Evars/Metas switching...} *)
 
 (** [evars_to_metas] generates new metavariables for each non dependent
    existential and performs the replacement in the given constr; it also
@@ -66,10 +62,9 @@ val evars_to_metas : evar_map -> open_constr -> (evar_map * constr)
 
 val non_instantiated : evar_map -> (evar * evar_info) list
 
-(**********************************************************
-   Unification utils *)
+(** {6 Unification utils} *)
 
-(** [head_evar c} returns the head evar of [c] if any *)
+(** [head_evar c] returns the head evar of [c] if any *)
 exception NoHeadEvar
 val head_evar : constr -> existential_key (** may raise NoHeadEvar *)
 
@@ -105,8 +100,7 @@ val evars_of_term : constr -> Intset.t
 val evars_of_named_context : named_context -> Intset.t
 val evars_of_evar_info : evar_info -> Intset.t
 
-(**********************************************************
-   Value/Type constraints *)
+(** {6 Value/Type constraints} *)
 
 val judge_of_new_Type : unit -> unsafe_judgment
 
@@ -166,16 +160,14 @@ val flush_and_check_evars :  evar_map -> constr -> constr
    their representative that is most ancient in the context *)
 val expand_vars_in_term : env -> constr -> constr
 
-(********************************************************************
-   debug pretty-printer: *)
+(** {6 debug pretty-printer:} *)
 
 val pr_tycon_type : env -> type_constraint_type -> Pp.std_ppcmds
 val pr_tycon : env -> type_constraint -> Pp.std_ppcmds
 
 
-(********************************************************************
-   Removing hyps in evars'context;                                   
-   raise OccurHypInSimpleClause if the removal breaks dependencies   *)
+(** {6 Removing hyps in evars'context}
+raise OccurHypInSimpleClause if the removal breaks dependencies *)
 
 type clear_dependency_error =
 | OccurHypInSimpleClause of identifier option
@@ -183,14 +175,14 @@ type clear_dependency_error =
 
 exception ClearDependencyError of identifier * clear_dependency_error
 
-(* spiwack: marks an evar that has been "defined" by clear. 
+(* spiwack: marks an evar that has been "defined" by clear.
     used by [Goal] and (indirectly) [Proofview] to handle the clear tactic gracefully*)
 val cleared : bool Store.Field.t
 
 val clear_hyps_in_evi : evar_map ref -> named_context_val -> types ->
   identifier list -> named_context_val * types
 
-val push_rel_context_to_named_context : Environ.env -> types -> 
+val push_rel_context_to_named_context : Environ.env -> types ->
   named_context_val * types * constr list
 
 val generalize_evar_over_rels : evar_map -> existential -> types * constr list
diff --git a/pretyping/glob_term.mli b/pretyping/glob_term.mli
index 4e11221d8..9649ad2c0 100644
--- a/pretyping/glob_term.mli
+++ b/pretyping/glob_term.mli
@@ -21,11 +21,11 @@ open Nametab
 
 (**  The kind of patterns that occurs in "match ... with ... end"
 
-     locs here refers to the ident's location, not whole pat the last
-     argument of PatCstr is a possible alias ident for the pattern *)
+     locs here refers to the ident's location, not whole pat *)
 type cases_pattern =
   | PatVar of loc * name
-  | PatCstr of loc * constructor * cases_pattern list * name
+  | PatCstr of loc * constructor * cases_pattern list * name 
+      (** [PatCstr(p,C,l,x)] = "|'C' 'l' as 'x'" *)
 
 val cases_pattern_loc : cases_pattern -> loc
 
@@ -60,6 +60,9 @@ type glob_constr =
   | GProd of loc * name * binding_kind * glob_constr * glob_constr
   | GLetIn of loc * name * glob_constr * glob_constr
   | GCases of loc * case_style * glob_constr option * tomatch_tuples * cases_clauses
+      (** [GCases(l,style,r,tur,cc)] = "match 'tur' return 'r' with 'cc'" (in 
+	  [MatchStyle]) *)
+
   | GLetTuple of loc * name list * (name * glob_constr option) *
       glob_constr * glob_constr
   | GIf of loc * glob_constr * (name * glob_constr option) * glob_constr * glob_constr
@@ -80,12 +83,15 @@ and fix_kind =
 
 and predicate_pattern =
     name * (loc * inductive * int * name list) option
+      (** [(na,id)] = "as 'na' in 'id'" where if [id] is [Some(l,I,k,args)], [k]
+	  is the number of parameter of [I]. *)
 
 and tomatch_tuple = (glob_constr * predicate_pattern)
 
 and tomatch_tuples = tomatch_tuple list
 
 and cases_clause = (loc * identifier list * cases_pattern list * glob_constr)
+(** [(p,il,cl,t)] = "|'cl' as 'il' => 't'" *)
 
 and cases_clauses = cases_clause list
 
@@ -113,7 +119,6 @@ val loc_of_glob_constr : glob_constr -> loc
     
     Take the current alias as parameter, 
     @raise Not_found if translation is impossible *)
-
 val cases_pattern_of_glob_constr : name -> glob_constr -> cases_pattern
 
 val glob_constr_of_closed_cases_pattern : cases_pattern -> name * glob_constr