Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg

10 files changed, 152 insertions, 204 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 141e8f8a..efb6c853 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: constrextern.ml 11024 2008-05-30 12:41:39Z msozeau $ *)
+(* $Id: constrextern.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
 
 (*i*)
 open Pp
@@ -98,7 +98,7 @@ let ids_of_ctxt ctxt =
        (function c -> match kind_of_term c with
 	  | Var id -> id
 	  | _ ->
-       error "arbitrary substitution of references not implemented")
+       error "Arbitrary substitution of references not implemented.")
      ctxt)
 
 let idopt_of_name = function 
@@ -973,7 +973,7 @@ and raw_of_eqn env constr construct_nargs branch =
             buildrec new_ids (pat::patlist) new_env (n-1) b
 
 	| _ ->
-	    error "Unsupported branch in case-analysis while printing pattern"
+	    error "Unsupported branch in case-analysis while printing pattern."
   in 
   buildrec [] [] env construct_nargs branch
 
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 9abee4d4..9af7e769 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: constrintern.ml 11065 2008-06-06 22:39:43Z msozeau $ *)
+(* $Id: constrintern.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
 
 open Pp
 open Util
@@ -50,7 +50,7 @@ let for_grammar f x =
 type internalisation_error =
   | VariableCapture of identifier
   | WrongExplicitImplicit
-  | NegativeMetavariable
+  | IllegalMetavariable
   | NotAConstructor of reference
   | UnboundFixName of bool * identifier
   | NonLinearPattern of identifier
@@ -66,8 +66,8 @@ let explain_wrong_explicit_implicit =
   str "Found an explicitly given implicit argument but was expecting" ++
   fnl () ++ str "a regular one"
 
-let explain_negative_metavariable =
-  str "Metavariable numbers must be positive"
+let explain_illegal_metavariable =
+  str "Metavariables allowed only in patterns"
 
 let explain_not_a_constructor ref =
   str "Unknown constructor: " ++ pr_reference ref
@@ -99,24 +99,26 @@ let explain_bad_explicitation_number n po =
       str "Bad explicitation name: found " ++ pr_id id ++ 
       str" but was expecting " ++ s
 
-let explain_internalisation_error = function
+let explain_internalisation_error e =
+  let pp = match e with
   | VariableCapture id -> explain_variable_capture id
   | WrongExplicitImplicit -> explain_wrong_explicit_implicit
-  | NegativeMetavariable -> explain_negative_metavariable
+  | IllegalMetavariable -> explain_illegal_metavariable
   | NotAConstructor ref -> explain_not_a_constructor ref
   | UnboundFixName (iscofix,id) -> explain_unbound_fix_name iscofix id
   | NonLinearPattern id -> explain_non_linear_pattern id
   | BadPatternsNumber (n1,n2) -> explain_bad_patterns_number n1 n2
-  | BadExplicitationNumber (n,po) -> explain_bad_explicitation_number n po
+  | BadExplicitationNumber (n,po) -> explain_bad_explicitation_number n po in
+  pp ++ str "."
 
 let error_unbound_patvar loc n =
   user_err_loc
     (loc,"glob_qualid_or_patvar", str "?" ++ pr_patvar n ++ 
-      str " is unbound")
+      str " is unbound.")
 
 let error_bad_inductive_type loc =
   user_err_loc (loc,"",str 
-    "This should be an inductive type applied to names or \"_\"")
+    "This should be an inductive type applied to names or \"_\".")
 
 let error_inductive_parameter_not_implicit loc =
   user_err_loc (loc,"", str
@@ -324,7 +326,7 @@ let set_var_scope loc id (_,scopt,scopes) varscopes =
     make_current_scope (Option.get !idscopes)
     <> make_current_scope (scopt,scopes) then
       user_err_loc (loc,"set_var_scope",
-      pr_id id ++ str " already occurs in a different scope")
+      pr_id id ++ str " already occurs in a different scope.")
   else
     idscopes := Some (scopt,scopes)
 
@@ -444,7 +446,7 @@ let intern_var (env,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) loc id =
   try
     match List.assoc id unbndltacvars with
       | None -> user_err_loc (loc,"intern_var",
-	  str "variable " ++ pr_id id ++ str " should be bound to a term")
+	  str "variable " ++ pr_id id ++ str " should be bound to a term.")
       | Some id0 -> Pretype_errors.error_var_not_found_loc loc id0
   with Not_found ->
   (* Is [id] a goal or section variable *)
@@ -463,14 +465,14 @@ let find_appl_head_data (_,_,_,(_,impls)) = function
   | x -> x,[],[],[]
 
 let error_not_enough_arguments loc =
-  user_err_loc (loc,"",str "Abbreviation is not applied enough")
+  user_err_loc (loc,"",str "Abbreviation is not applied enough.")
 
 let check_no_explicitation l =
   let l = List.filter (fun (a,b) -> b <> None) l in
   if l <> [] then
     let loc = fst (Option.get (snd (List.hd l))) in
     user_err_loc
-      (loc,"",str"Unexpected explicitation of the argument of an abbreviation")
+     (loc,"",str"Unexpected explicitation of the argument of an abbreviation.")
 
 (* Is it a global reference or a syntactic definition? *)
 let intern_qualid loc qid intern env args =
@@ -580,7 +582,7 @@ let check_number_of_pattern loc n l =
 let check_or_pat_variables loc ids idsl =
   if List.exists (fun ids' -> not (list_eq_set ids ids')) idsl then
     user_err_loc (loc, "", str 
-    "The components of this disjunctive pattern must bind the same variables")
+    "The components of this disjunctive pattern must bind the same variables.")
 
 let check_constructor_length env loc cstr pl pl0 =
   let n = List.length pl + List.length pl0 in
@@ -607,7 +609,7 @@ let message_redundant_alias (id1,id2) =
 (* Expanding notations *)
 
 let error_invalid_pattern_notation loc =
-  user_err_loc (loc,"",str "Invalid notation for pattern")
+  user_err_loc (loc,"",str "Invalid notation for pattern.")
 
 let chop_aconstr_constructor loc (ind,k) args =
   let nparams = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in
@@ -815,9 +817,9 @@ let locate_if_isevar loc na = function
 
 let check_hidden_implicit_parameters id (_,_,_,(indnames,_)) =
   if List.mem id indnames then
-    errorlabstrm "" (str "A parameter or name of an inductive type " ++
-    pr_id id ++ str " must not be used as a bound variable in the type \
-of its constructor")
+    errorlabstrm "" (strbrk "A parameter or name of an inductive type " ++
+    pr_id id ++ strbrk " must not be used as a bound variable in the type \
+of its constructor.")
 
 let push_name_env lvar (ids,tmpsc,scopes as env) = function
   | Anonymous -> env 
@@ -840,11 +842,9 @@ let intern_typeclass_binders intern_type lvar env bl =
 	(env, (na,bk,None,ty)::bl))
     env bl
 
-let intern_typeclass_binder intern_type lvar (env,bl) na b ty =
-  let ctx = (na, b, ty) in
-  let (fvs, bind) = Implicit_quantifiers.generalize_class_binders_raw (pi1 env) [ctx] in
-  let env, ifvs = intern_typeclass_binders intern_type lvar (env,bl) fvs in
-    intern_typeclass_binders intern_type lvar (env,ifvs) bind
+let intern_typeclass_binder intern_type lvar (env,bl) cb =
+  let (ids, fvs, bind) = Implicit_quantifiers.generalize_class_binder_raw (pi1 env) cb in
+    intern_typeclass_binders intern_type lvar (env,bl) (fvs@[bind])
     
 let intern_local_binder_aux intern intern_type lvar ((ids,ts,sc as env),bl) = function
   | LocalRawAssum(nal,bk,ty) ->
@@ -857,8 +857,8 @@ let intern_local_binder_aux intern intern_type lvar ((ids,ts,sc as env),bl) = fu
 		(fun ((ids,ts,sc),bl) (_,na) ->
 		  ((name_fold Idset.add na ids,ts,sc), (na,k,None,ty)::bl))
 		(env,bl) nal
-	| TypeClass b ->
-	    intern_typeclass_binder intern_type lvar (env,bl) (List.hd nal) b ty)
+	| TypeClass (b,b') ->
+	    intern_typeclass_binder intern_type lvar (env,bl) (List.hd nal, (b,b'), ty))
   | LocalRawDef((loc,na),def) ->
       ((name_fold Idset.add na ids,ts,sc),
       (na,Explicit,Some(intern env def),RHole(loc,Evd.BinderType na))::bl)
@@ -880,11 +880,11 @@ let check_projection isproj nargs r =
       (try
 	let n = Recordops.find_projection_nparams ref + 1 in
 	if nargs <> n then
-	  user_err_loc (loc,"",str "Projection has not the right number of explicit parameters");
+	  user_err_loc (loc,"",str "Projection has not the right number of explicit parameters.");
       with Not_found -> 
 	user_err_loc
-	(loc,"",pr_global_env Idset.empty ref ++ str " is not a registered projection"))
-  | _, Some _ -> user_err_loc (loc_of_rawconstr r, "", str "Not a projection")
+	(loc,"",pr_global_env Idset.empty ref ++ str " is not a registered projection."))
+  | _, Some _ -> user_err_loc (loc_of_rawconstr r, "", str "Not a projection.")
   | _, None -> ()
 
 let get_implicit_name n imps =
@@ -909,10 +909,11 @@ let extract_explicit_arg imps args =
 	  let id = match pos with
 	  | ExplByName id ->
 	      if not (exists_implicit_name id imps) then
-		user_err_loc (loc,"",str "Wrong argument name: " ++ pr_id id);
+		user_err_loc
+		  (loc,"",str "Wrong argument name: " ++ pr_id id ++ str ".");
 	      if List.mem_assoc id eargs then
 		user_err_loc (loc,"",str "Argument name " ++ pr_id id
-		++ str " occurs more than once");
+		++ str " occurs more than once.");
 	      id
 	  | ExplByPos (p,_id) ->
 	      let id =
@@ -921,11 +922,12 @@ let extract_explicit_arg imps args =
 		  if not (is_status_implicit imp) then failwith "imp";
 		  name_of_implicit imp
 		with Failure _ (* "nth" | "imp" *) ->
-		  user_err_loc (loc,"",str"Wrong argument position: " ++ int p)
+		  user_err_loc
+		    (loc,"",str"Wrong argument position: " ++ int p ++ str ".")
 	      in
 	      if List.mem_assoc id eargs then
 		user_err_loc (loc,"",str"Argument at position " ++ int p ++
-		  str " is mentioned more than once");
+		  str " is mentioned more than once.");
 	      id in
 	  ((id,(loc,a))::eargs,rargs)
   in aux args
@@ -1086,7 +1088,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
     | CPatVar (loc, n) when allow_patvar ->
 	RPatVar (loc, n)
     | CPatVar (loc, _) ->
-	raise (InternalisationError (loc,NegativeMetavariable))
+	raise (InternalisationError (loc,IllegalMetavariable))
     | CEvar (loc, n, l) ->
 	REvar (loc, n, Option.map (List.map (intern env)) l)
     | CSort (loc, s) ->
@@ -1149,7 +1151,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
 	let nal = List.map (function
 	  | RHole loc -> Anonymous
 	  | RVar (_,id) -> Name id
-	  | c -> user_err_loc (loc_of_rawconstr c,"",str "Not a name")) l in
+	  | c -> user_err_loc (loc_of_rawconstr c,"",str "Not a name.")) l in
 	let parnal,realnal = list_chop nparams nal in
 	if List.exists ((<>) Anonymous) parnal then
 	  error_inductive_parameter_not_implicit loc;
@@ -1173,9 +1175,9 @@ let internalise sigma globalenv env allow_patvar lvar c =
     in
       match bk with
 	| Default b -> default env b nal
-	| TypeClass b -> 
+	| TypeClass (b,b') -> 
 	    let env, ibind = intern_typeclass_binder intern_type lvar
-	      (env, []) (List.hd nal) b ty in
+	      (env, []) (List.hd nal,(b,b'),ty) in
 	    let body = intern_type env body in
 	      it_mkRProd ibind body
 					   
@@ -1189,9 +1191,9 @@ let internalise sigma globalenv env allow_patvar lvar c =
       | [] -> intern env body
     in match bk with
       | Default b -> default env b nal
-      | TypeClass b ->	  
+      | TypeClass (b, b') ->	  
 	  let env, ibind = intern_typeclass_binder intern_type lvar
-	    (env, []) (List.hd nal) b ty in
+	    (env, []) (List.hd nal,(b,b'),ty) in
 	  let body = intern env body in
 	    it_mkRLambda ibind body
 	      
@@ -1221,7 +1223,8 @@ let internalise sigma globalenv env allow_patvar lvar c =
 	  if eargs <> [] then 
 	    (let (id,(loc,_)) = List.hd eargs in
 	       user_err_loc (loc,"",str "Not enough non implicit
-	    arguments to accept the argument bound to " ++ pr_id id));
+	    arguments to accept the argument bound to " ++ 
+		 pr_id id ++ str"."));
 	  []
       | ([], rargs) ->
 	  assert (eargs = []);
@@ -1275,23 +1278,6 @@ let intern_ltac isarity ltacvars sigma env c =
 
 type manual_implicits = (explicitation * (bool * bool)) list
 
-let implicits_of_rawterm l = 
-  let rec aux i c = 
-    match c with
-	RProd (loc, na, bk, t, b) | RLambda (loc, na, bk, t, b) -> 
-	  let rest = aux (succ i) b in
-	    if bk = Implicit then
-	      let name =
-		match na with
-		    Name id -> Some id
-		  | Anonymous -> None
-	      in
-		(ExplByPos (i, name), (true, true)) :: rest
-	    else rest
-      | RLetIn (loc, na, t, b) -> aux i b
-      | _ -> []
-  in aux 1 l
-
 (*********************************************************************)
 (* Functions to parse and interpret constructions *)
 
@@ -1321,11 +1307,11 @@ let interp_constr_evars_gen_impls ?evdref
   match evdref with 
     | None -> 
 	let c = intern_gen (kind=IsType) ~impls Evd.empty env c in
-	let imps = implicits_of_rawterm c in
+	let imps = Implicit_quantifiers.implicits_of_rawterm c in
 	  Default.understand_gen kind Evd.empty env c, imps
     | Some evdref ->
 	let c = intern_gen (kind=IsType) ~impls (Evd.evars_of !evdref) env c in
-	let imps = implicits_of_rawterm c in
+	let imps = Implicit_quantifiers.implicits_of_rawterm c in
 	  Default.understand_tcc_evars evdref env kind c, imps
 
 let interp_constr_evars_gen evdref env ?(impls=([],[])) kind c =
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 65e4dcd5..ca758458 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coqlib.ml 11072 2008-06-08 16:13:37Z herbelin $ *)
+(* $Id: coqlib.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
 
 open Util
 open Pp
@@ -70,7 +70,7 @@ let check_required_library d =
      (dummy_loc,make_qualid (make_dirpath (List.rev prefix)) m)
 *)
 (* or failing ...*)
-    error ("Library "^(string_of_dirpath dir)^" has to be required first")
+    error ("Library "^(string_of_dirpath dir)^" has to be required first.")
 
 (************************************************************************)
 (* Specific Coq objects *)
diff --git a/interp/genarg.ml b/interp/genarg.ml
index 49c157f2..c54dfe23 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: genarg.ml 10753 2008-04-04 14:55:47Z herbelin $ *)
+(* $Id: genarg.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
 
 open Pp
 open Util
@@ -75,24 +75,24 @@ let create_arg s =
 let exists_argtype s = List.mem s !dyntab
 
 type intro_pattern_expr =
-  | IntroOrAndPattern of case_intro_pattern_expr
+  | IntroOrAndPattern of or_and_intro_pattern_expr
   | IntroWildcard
-  | IntroIdentifier of identifier
-  | IntroAnonymous
   | IntroRewrite of bool
+  | IntroIdentifier of identifier
   | IntroFresh of identifier
-and case_intro_pattern_expr = intro_pattern_expr list list
+  | IntroAnonymous
+and or_and_intro_pattern_expr = (loc * intro_pattern_expr) list list
 
-let rec pr_intro_pattern = function
-  | IntroOrAndPattern pll -> pr_case_intro_pattern pll
+let rec pr_intro_pattern (_,pat) = match pat with
+  | IntroOrAndPattern pll -> pr_or_and_intro_pattern pll
   | IntroWildcard -> str "_"
-  | IntroIdentifier id -> pr_id id
-  | IntroAnonymous -> str "?"
   | IntroRewrite true -> str "->"
   | IntroRewrite false -> str "<-"
+  | IntroIdentifier id -> pr_id id
   | IntroFresh id -> str "?" ++ pr_id id
+  | IntroAnonymous -> str "?"
 
-and pr_case_intro_pattern = function
+and pr_or_and_intro_pattern = function
   | [pl] ->
       str "(" ++ hv 0 (prlist_with_sep pr_coma pr_intro_pattern pl) ++ str ")"
   | pll ->
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 3548585b..da175078 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: genarg.mli 10753 2008-04-04 14:55:47Z herbelin $ i*)
+(*i $Id: genarg.mli 11309 2008-08-06 10:30:35Z herbelin $ i*)
 
 open Util
 open Names
@@ -32,16 +32,16 @@ type open_rawconstr = unit * rawconstr_and_expr
 type 'a with_ebindings = 'a * open_constr bindings
 
 type intro_pattern_expr =
-  | IntroOrAndPattern of case_intro_pattern_expr
+  | IntroOrAndPattern of or_and_intro_pattern_expr
   | IntroWildcard
-  | IntroIdentifier of identifier
-  | IntroAnonymous
   | IntroRewrite of bool
+  | IntroIdentifier of identifier
   | IntroFresh of identifier
-and case_intro_pattern_expr = intro_pattern_expr list list
+  | IntroAnonymous
+and or_and_intro_pattern_expr = (loc * intro_pattern_expr) list list
 
-val pr_intro_pattern : intro_pattern_expr -> Pp.std_ppcmds
-val pr_case_intro_pattern : case_intro_pattern_expr -> Pp.std_ppcmds
+val pr_intro_pattern : intro_pattern_expr located -> Pp.std_ppcmds
+val pr_or_and_intro_pattern : or_and_intro_pattern_expr -> Pp.std_ppcmds
 
 (* The route of a generic argument, from parsing to evaluation
 
@@ -128,15 +128,16 @@ val wit_int_or_var : (int or_var,tlevel) abstract_argument_type
 
 val rawwit_string : (string,rlevel) abstract_argument_type
 val globwit_string : (string,glevel) abstract_argument_type
+
 val wit_string : (string,tlevel) abstract_argument_type
 
 val rawwit_pre_ident : (string,rlevel) abstract_argument_type
 val globwit_pre_ident : (string,glevel) abstract_argument_type
 val wit_pre_ident : (string,tlevel) abstract_argument_type
 
-val rawwit_intro_pattern : (intro_pattern_expr,rlevel) abstract_argument_type
-val globwit_intro_pattern : (intro_pattern_expr,glevel) abstract_argument_type
-val wit_intro_pattern : (intro_pattern_expr,tlevel) abstract_argument_type
+val rawwit_intro_pattern : (intro_pattern_expr located,rlevel) abstract_argument_type
+val globwit_intro_pattern : (intro_pattern_expr located,glevel) abstract_argument_type
+val wit_intro_pattern : (intro_pattern_expr located,tlevel) abstract_argument_type
 
 val rawwit_ident : (identifier,rlevel) abstract_argument_type
 val globwit_ident : (identifier,glevel) abstract_argument_type
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index d480ad39..a83071d1 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: implicit_quantifiers.ml 10922 2008-05-12 12:47:17Z msozeau $ i*)
+(*i $Id: implicit_quantifiers.ml 11282 2008-07-28 11:51:53Z msozeau $ i*)
 
 (*i*)
 open Names
@@ -29,7 +29,6 @@ open Pp
 let ids_of_list l = 
   List.fold_right Idset.add l Idset.empty
 
-
 let locate_reference qid =
   match Nametab.extended_locate qid with
     | TrueGlobal ref -> true
@@ -88,44 +87,17 @@ let rec make_fresh ids env x =
 let freevars_of_ids env ids = 
   List.filter (is_freevar env (Global.env())) ids
 
-let compute_constrs_freevars env constrs =
-  let ids = 
-    List.rev (List.fold_left 
-		 (fun acc x -> free_vars_of_constr_expr x acc) 
-		 [] constrs)
-  in freevars_of_ids env ids
-
-(* let compute_context_freevars env ctx = *)
-(*   let ids = *)
-(*     List.rev *)
-(*       (List.fold_left *)
-(* 	  (fun acc (_,i,x) -> free_vars_of_constr_expr x acc) *)
-(* 	  [] constrs) *)
-(*   in freevars_of_ids ids *)
-
-let compute_constrs_freevars_binders env constrs =
-  let elts = compute_constrs_freevars env constrs in
-    List.map (fun id -> (dummy_loc, id), CHole (dummy_loc, None)) elts
-
 let binder_list_of_ids ids =
   List.map (fun id -> LocalRawAssum ([dummy_loc, Name id], Default Implicit, CHole (dummy_loc, None))) ids
       
 let next_ident_away_from id avoid = make_fresh avoid (Global.env ()) id
-(*   let rec name_rec id = *)
-(*     if Idset.mem id avoid then name_rec (Nameops.lift_ident id) else id in  *)
-(*   name_rec id  *)
-
-let ids_of_named_context_avoiding avoid l =
-  List.fold_left (fun (ids, avoid) id -> 
-    let id' = next_ident_away_from id avoid in id' :: ids, Idset.add id' avoid) 
-    ([], avoid) (Termops.ids_of_named_context l)
     
 let combine_params avoid fn applied needed =
   let named, applied = 
     List.partition 
       (function
 	  (t, Some (loc, ExplByName id)) -> 
-	    if not (List.exists (fun (_, (id', _, _)) -> id = id') needed) then
+	    if not (List.exists (fun (_, (id', _, _)) -> Name id = id') needed) then
 	      user_err_loc (loc,"",str "Wrong argument name: " ++ Nameops.pr_id id);
 	    true
 	| _ -> false) applied
@@ -138,13 +110,13 @@ let combine_params avoid fn applied needed =
     match app, need with
 	[], [] -> List.rev ids, avoid
 
-      | app, (_, (id, _, _)) :: need when List.mem_assoc id named ->
+      | app, (_, (Name id, _, _)) :: need when List.mem_assoc id named ->
 	  aux (List.assoc id named :: ids) avoid app need
 	    
-      | (x, None) :: app, (None, (id, _, _)) :: need ->
+      | (x, None) :: app, (None, (Name id, _, _)) :: need ->
 	  aux (x :: ids) avoid app need
 	    
-      | _, (Some cl, (id, _, _) as d) :: need -> 
+      | _, (Some cl, (Name id, _, _) as d) :: need -> 
 	  let t', avoid' = fn avoid d in
 	    aux (t' :: ids) avoid' app need
 
@@ -155,12 +127,14 @@ let combine_params avoid fn applied needed =
 	    aux (t' :: ids) avoid' app need
 
       | _ :: _, [] -> failwith "combine_params: overly applied typeclass"
+
+      | _, _ -> raise (Invalid_argument "combine_params")
   in aux [] avoid applied needed
 
 let combine_params_freevar avoid applied needed =
   combine_params avoid
     (fun avoid (_, (id, _, _)) -> 
-      let id' = next_ident_away_from id avoid in
+      let id' = next_ident_away_from (Nameops.out_name id) avoid in
 	(CRef (Ident (dummy_loc, id')), Idset.add id' avoid))
     applied needed
 
@@ -201,19 +175,6 @@ let full_class_binders env l =
 	| Explicit -> (x :: l', avoid))
       ([], avoid) l
   in List.rev l'
-      
-let constr_expr_of_constraint (kind, id) l =
-  match kind with
-    | Implicit -> CAppExpl (fst id, (None, Ident id), l)
-    | Explicit -> CApp (fst id, (None, CRef (Ident id)),
-		       List.map (fun x -> x, None) l)
-
-(*    | CApp of loc * (proj_flag * constr_expr) *  *)
-(*         (constr_expr * explicitation located option) list *)
-
-
-let constrs_of_context l =
-  List.map (fun (_, id, l) -> constr_expr_of_constraint id l) l
 
 let compute_context_freevars env ctx =
   let bound, ids = 
@@ -232,41 +193,50 @@ let resolve_class_binders env l =
   in
     fv_ctx, ctx
 
-let generalize_class_binders env l = 
-  let fv_ctx, cstrs = resolve_class_binders env l in
-    List.map (fun ((loc, id), t) -> LocalRawAssum ([loc, Name id], Default Implicit, t)) fv_ctx,
-  List.map (fun (iid, bk, c) -> LocalRawAssum ([iid], Default Implicit, c)) 
-    cstrs
+let full_class_binder env (iid, (bk, bk'), cl as c) = 
+  let avoid = Idset.union env (ids_of_list (compute_context_vars env [c])) in
+  let c, avoid =
+    match bk' with
+    | Implicit -> 
+	let (loc, id, l) = 
+	  try destClassAppExpl cl 
+	  with Not_found -> 
+	    user_err_loc (constr_loc cl, "class_binders", str"Not an applied type class")
+	in
+	let gr = Nametab.global id in
+	  (try
+	      let c = class_info gr in
+	      let args, avoid = combine_params_freevar avoid l (List.rev c.cl_context) in
+		(iid, bk, CAppExpl (loc, (None, id), args)), avoid
+	    with Not_found -> not_a_class (Global.env ()) (constr_of_global gr))
+    | Explicit -> ((iid,bk,cl), avoid)
+  in c
+
+let compute_constraint_freevars env (oid, _, x) =
+  let bound = match snd oid with Name n -> Idset.add n env | Anonymous -> env in
+  let ids = free_vars_of_constr_expr x ~bound [] in
+    freevars_of_ids env (List.rev ids)
+
+let resolve_class_binder env c = 
+  let cstr = full_class_binder env c in
+  let fv_ctx = 
+    let elts = compute_constraint_freevars env cstr in
+      List.map (fun id -> (dummy_loc, id), CHole (dummy_loc, None)) elts
+  in fv_ctx, cstr
+    
+let generalize_class_binder_raw env c = 
+  let env = Idset.union env (Termops.vars_of_env (Global.env())) in
+  let fv_ctx, cstr = resolve_class_binder env c in
+  let ids' = List.fold_left (fun acc ((loc, id), t) -> Idset.add id acc) env fv_ctx in
+  let ctx' = List.map (fun ((loc, id), t) -> ((loc, Name id), Implicit, t)) fv_ctx in
+    ids', ctx', cstr
 
 let generalize_class_binders_raw env l = 
   let env = Idset.union env (Termops.vars_of_env (Global.env())) in
   let fv_ctx, cstrs = resolve_class_binders env l in
     List.map (fun ((loc, id), t) -> ((loc, Name id), Implicit, t)) fv_ctx,
   List.map (fun (iid, bk, c) -> (iid, Implicit, c)) cstrs
-
-let ctx_of_class_binders env l = 
-  let (x, y) = generalize_class_binders env l in x @ y
 	
-let implicits_of_binders l = 
-  let rec aux i l = 
-    match l with 
-	[] -> []
-      | hd :: tl -> 
-	  let res, reslen = 
-	    match hd with
-		LocalRawAssum (nal, Default Implicit, t) -> 
-		  list_map_i (fun i (_,id) ->
-		    let name =
-		      match id with
-			  Name id -> Some id
-			| Anonymous -> None
-		    in ExplByPos (i, name), (true, true))
-		    i nal, List.length nal
-	      | LocalRawAssum (nal, _, _) -> [], List.length nal
-	      | LocalRawDef _ -> [], 1
-	  in res @ (aux (i + reslen) tl)
-  in aux 1 l
-  
 let implicits_of_rawterm l = 
   let rec aux i c = 
     match c with
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index ff81dc10..1ee81ce9 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: implicit_quantifiers.mli 10739 2008-04-01 14:45:20Z herbelin $ i*)
+(*i $Id: implicit_quantifiers.mli 11282 2008-07-28 11:51:53Z msozeau $ i*)
 
 (*i*)
 open Names
@@ -39,30 +39,23 @@ val make_fresh : Names.Idset.t -> Environ.env -> identifier -> identifier
 val free_vars_of_binders :
   ?bound:Idset.t -> Names.identifier list -> local_binder list -> Idset.t * Names.identifier list
 
-val compute_constrs_freevars : Idset.t -> constr_expr list -> identifier list
-val compute_constrs_freevars_binders : Idset.t -> constr_expr list -> (identifier located * constr_expr) list
 val resolve_class_binders : Idset.t -> typeclass_context -> 
   (identifier located * constr_expr) list * typeclass_context
 
 val full_class_binders : Idset.t -> typeclass_context -> typeclass_context
+
+val generalize_class_binder_raw : Idset.t -> name located * (binding_kind * binding_kind) * constr_expr -> 
+  Idset.t * typeclass_context * typeclass_constraint
   
 val generalize_class_binders_raw : Idset.t -> typeclass_context -> 
   (name located * binding_kind * constr_expr) list * (name located * binding_kind * constr_expr) list
 
-val ctx_of_class_binders : Idset.t -> typeclass_context -> local_binder list
-
-val implicits_of_binders : local_binder list -> (Topconstr.explicitation * (bool * bool)) list
-
 val implicits_of_rawterm : Rawterm.rawconstr -> (Topconstr.explicitation * (bool * bool)) list
 
 val combine_params : Names.Idset.t ->
-  (Names.Idset.t -> (global_reference * bool) option * (Names.identifier * Term.constr option * Term.types) ->
+  (Names.Idset.t -> (global_reference * bool) option * (Names.name * Term.constr option * Term.types) ->
     Topconstr.constr_expr * Names.Idset.t) ->
   (Topconstr.constr_expr * Topconstr.explicitation located option) list ->
-  ((global_reference * bool) option * Term.named_declaration) list ->
+  ((global_reference * bool) option * Term.rel_declaration) list ->
   Topconstr.constr_expr list * Names.Idset.t
 
-
-val ids_of_named_context_avoiding :     Names.Idset.t ->
-    Sign.named_context -> Names.Idset.elt list * Names.Idset.t
-
diff --git a/interp/notation.ml b/interp/notation.ml
index 98a199ad..9e83b860 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: notation.ml 10893 2008-05-07 09:20:43Z herbelin $ *)
+(* $Id: notation.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
 
 (*i*)
 open Util
@@ -78,7 +78,7 @@ let declare_scope scope =
 
 let find_scope scope =
   try Gmap.find scope !scope_map
-  with Not_found -> error ("Scope "^scope^" is not declared")
+  with Not_found -> error ("Scope "^scope^" is not declared.")
 
 let check_scope sc = let _ = find_scope sc in ()
 
@@ -159,7 +159,7 @@ let find_delimiters_scope loc key =
   try Gmap.find key !delimiters_map
   with Not_found -> 
     user_err_loc 
-    (loc, "find_delimiters", str ("Unknown scope delimiting key "^key))
+    (loc, "find_delimiters", str ("Unknown scope delimiting key "^key^"."))
 
 (* Uninterpretation tables *)
 
@@ -251,7 +251,7 @@ let check_required_module loc sc (sp,d) =
   with Not_found ->
     user_err_loc (loc,"prim_token_interpreter",
     str ("Cannot interpret in "^sc^" without requiring first module "
-    ^(list_last d)))
+    ^(list_last d)^"."))
 
 (* Look if some notation or numeral printer in [scope] can be used in
    the scope stack [scopes], and if yes, using delimiters or not *)
@@ -348,7 +348,7 @@ let interp_prim_token_gen g loc p local_scopes =
     user_err_loc (loc,"interp_prim_token",
     (match p with
       | Numeral n -> str "No interpretation for numeral " ++ pr_bigint n
-      | String s -> str "No interpretation for string " ++ qs s))
+      | String s -> str "No interpretation for string " ++ qs s) ++ str ".")
 
 let interp_prim_token =
   interp_prim_token_gen (fun x -> x)
@@ -361,7 +361,7 @@ let rec interp_notation loc ntn local_scopes =
   try find_interpretation (find_notation ntn) scopes
   with Not_found ->
     user_err_loc
-    (loc,"",str ("Unknown interpretation for notation \""^ntn^"\""))
+    (loc,"",str ("Unknown interpretation for notation \""^ntn^"\"."))
 
 let uninterp_notations c =
   Gmapl.find (rawconstr_key c) !notations_key_table
@@ -464,10 +464,10 @@ let subst_arguments_scope (_,subst,(req,r,scl)) =
   (ArgsScopeNoDischarge,fst (subst_global subst r),scl)
 
 let discharge_arguments_scope (_,(req,r,l)) =
-  if req = ArgsScopeNoDischarge then None
-  else Some (req,pop_global_reference r,l)
+  if req = ArgsScopeNoDischarge or (isVarRef r & Lib.is_in_section r) then None
+  else Some (req,Lib.discharge_global r,l)
 
-let rebuild_arguments_scope (_,(req,r,l)) =
+let rebuild_arguments_scope (req,r,l) =
   match req with
     | ArgsScopeNoDischarge -> assert false
     | ArgsScopeAuto ->
@@ -493,8 +493,7 @@ let declare_arguments_scope_gen req r scl =
   Lib.add_anonymous_leaf (inArgumentsScope (req,r,scl))
 
 let declare_arguments_scope local ref scl =
-  let req =
-    if local or isVarRef ref then ArgsScopeNoDischarge else ArgsScopeManual in
+  let req = if local then ArgsScopeNoDischarge else ArgsScopeManual in
   declare_arguments_scope_gen req ref scl
 
 let find_arguments_scope r =
@@ -503,8 +502,7 @@ let find_arguments_scope r =
 
 let declare_ref_arguments_scope ref =
   let t = Global.type_of_global ref in
-  let req = if isVarRef ref then ArgsScopeNoDischarge else ArgsScopeAuto in
-  declare_arguments_scope_gen req ref (compute_arguments_scope t)
+  declare_arguments_scope_gen ArgsScopeAuto ref (compute_arguments_scope t)
 
 (********************************)
 (* Encoding notations as string *)
@@ -627,12 +625,12 @@ let global_reference_of_notation test (ntn,(sc,c,_)) =
   | _ -> None
 
 let error_ambiguous_notation loc _ntn =
-  user_err_loc (loc,"",str "Ambiguous notation")
+  user_err_loc (loc,"",str "Ambiguous notation.")
 
 let error_notation_not_reference loc ntn =
   user_err_loc (loc,"",
     str "Unable to interpret " ++ quote (str ntn) ++
-    str " as a reference")
+    str " as a reference.")
 
 let interp_notation_as_global_reference loc test ntn =
   let ntns = browse_notation true ntn !scope_map in
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index b858eecb..a51b6bb0 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: topconstr.ml 11024 2008-05-30 12:41:39Z msozeau $ *)
+(* $Id: topconstr.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
 
 (*i*)
 open Pp
@@ -150,7 +150,7 @@ let compare_rawconstr f t1 t2 = match t1,t2 with
     | RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _),_
   | _,(RLetIn _ | RCases _ | RRec _ | RDynamic _
       | RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _)
-      -> error "Unsupported construction in recursive notations"
+      -> error "Unsupported construction in recursive notations."
   | (RRef _ | RVar _ | RApp _ | RLambda _ | RProd _ | RHole _ | RSort _), _
       -> false
 
@@ -168,13 +168,13 @@ let discriminate_patterns foundvars nl l1 l2 =
   | _ -> compare_rawconstr (aux (n+1)) c1 c2 in
   let l = list_map2_i aux 0 l1 l2 in
   if not (List.for_all ((=) true) l) then
-    error "Both ends of the recursive pattern differ";
+    error "Both ends of the recursive pattern differ.";
   match !diff with
-    | None ->  error "Both ends of the recursive pattern are the same"
+    | None ->  error "Both ends of the recursive pattern are the same."
     | Some (x,y,_ as discr) ->
 	List.iter (fun id ->
           if List.mem id !foundvars
-          then error "Variables used in the recursive part of a pattern are not allowed to occur outside of the recursive part";
+          then errorlabstrm "" (strbrk "Variables used in the recursive part of a pattern are not allowed to occur outside of the recursive part.");
           foundvars := id::!foundvars) [x;y];
 	discr
 
@@ -212,7 +212,7 @@ let aconstr_and_vars_of_rawconstr a =
       Array.iter (fun id -> found := id::!found) idl;
       let dll = Array.map (List.map (fun (na,bk,oc,b) -> 
 	 if bk <> Explicit then 
-	   error "Binders marked as implicit not allowed in notations";
+	   error "Binders marked as implicit not allowed in notations.";
 	 add_name found na; (na,Option.map aux oc,aux b))) dll in
       ARec (fk,idl,dll,Array.map aux tl,Array.map aux bl)
   | RCast (_,c,k) -> ACast (aux c, 
@@ -223,17 +223,17 @@ let aconstr_and_vars_of_rawconstr a =
   | RRef (_,r) -> ARef r
   | RPatVar (_,(_,n)) -> APatVar n
   | RDynamic _ | REvar _ ->
-      error "Existential variables not allowed in notations"
+      error "Existential variables not allowed in notations."
 
   (* Recognizing recursive notations *)
   and terminator_of_pat f1 ll1 lr1 = function
   | RApp (loc,f2,l2) ->
-      if not (eq_rawconstr f1 f2) then error
-	"Cannot recognize the same head to both ends of the recursive pattern";
+      if not (eq_rawconstr f1 f2) then errorlabstrm ""
+	(strbrk "Cannot recognize the same head to both ends of the recursive pattern.");
       let nl = List.length ll1 in
       let nr = List.length lr1 in
       if List.length l2 <> nl + nr + 1 then
-	error "Both ends of the recursive pattern have different lengths";
+	error "Both ends of the recursive pattern have different lengths.";
       let ll2,l2' = list_chop nl l2 in
       let t = List.hd l2' and lr2 = List.tl l2' in
       let x,y,order = discriminate_patterns found nl (ll1@lr1) (ll2@lr2) in
@@ -241,8 +241,8 @@ let aconstr_and_vars_of_rawconstr a =
         if order then RApp (loc,f2,ll2@RVar (loc,ldots_var)::lr2)
         else RApp (loc,f1,ll1@RVar (loc,ldots_var)::lr1) in
       (if order then y else x),(if order then x else y), aux iter, aux t, order
-  | _ -> error "One end of the recursive pattern is not an application"
-    
+  | _ -> error "One end of the recursive pattern is not an application."
+
   and make_aconstr_list f args =
     let rec find_patterns acc = function
       | RApp(_,RVar (_,a),[c]) :: l when a = ldots_var ->
@@ -250,7 +250,7 @@ let aconstr_and_vars_of_rawconstr a =
 	  let x,y,iter,term,lassoc = terminator_of_pat f (List.rev acc) l c in
 	  AList (x,y,iter,term,lassoc)
       | a::l -> find_patterns (a::acc) l
-      | [] -> error "Ill-formed recursive notation"
+      | [] -> error "Ill-formed recursive notation."
     in find_patterns [] args
 
   in
@@ -262,7 +262,7 @@ let aconstr_of_rawconstr vars a =
   let a,foundvars = aconstr_and_vars_of_rawconstr a in
   let check_type x =
     if not (List.mem x foundvars) then
-      error ((string_of_id x)^" is unbound in the right-hand-side") in
+      error ((string_of_id x)^" is unbound in the right-hand-side.") in
   List.iter check_type vars;
   a
 
@@ -590,7 +590,7 @@ type notation = string
 
 type explicitation = ExplByPos of int * identifier option | ExplByName of identifier
 
-type binder_kind = Default of binding_kind | TypeClass of binding_kind
+type binder_kind = Default of binding_kind | TypeClass of binding_kind * binding_kind
 
 type proj_flag = int option (* [Some n] = proj of the n-th visible argument *)
 
@@ -853,7 +853,7 @@ 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")
+         str "This expression should be a simple identifier.")
 
 (* Used in correctness and interface *)
 
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index d4fef0dc..2ac9da11 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: topconstr.mli 11024 2008-05-30 12:41:39Z msozeau $ i*)
+(*i $Id: topconstr.mli 11282 2008-07-28 11:51:53Z msozeau $ i*)
 
 (*i*)
 open Pp
@@ -95,7 +95,7 @@ type notation = string
 
 type explicitation = ExplByPos of int * identifier option | ExplByName of identifier
   
-type binder_kind = Default of binding_kind | TypeClass of binding_kind
+type binder_kind = Default of binding_kind | TypeClass of binding_kind * binding_kind
 
 type proj_flag = int option (* [Some n] = proj of the n-th visible argument *)