Imported Upstream version 8.0pl2upstream/8.0pl2

9 files changed, 188 insertions, 100 deletions

diff --git a/toplevel/class.ml b/toplevel/class.ml
index 429469b1..f5493929 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: class.ml,v 1.44.2.2 2004/07/16 19:31:47 herbelin Exp $ *)
+(* $Id: class.ml,v 1.44.2.3 2004/11/26 18:06:54 herbelin Exp $ *)
 
 open Util
 open Pp
@@ -92,15 +92,13 @@ let explain_coercion_error g = function
 
 (* Verifications pour l'ajout d'une classe *)
 
-let rec arity_sort a = match kind_of_term a with
-  | Sort (Prop _ | Type _) -> 0
-  | Prod (_,_,c) -> (arity_sort c) +1
-  | LetIn (_,_,_,c) -> arity_sort c    (* Utile ?? *)
-  | Cast (c,_) -> arity_sort c
+let rec arity_sort (ctx,a) = match kind_of_term a with
+  | Sort (Prop _ | Type _) -> List.length ctx
   | _ -> raise Not_found
 
 let check_reference_arity ref =
-  try arity_sort (Global.type_of_global ref)
+  let t = Global.type_of_global ref in
+  try arity_sort (Reductionops.splay_prod (Global.env()) Evd.empty t)
   with Not_found -> raise (CoercionError (NotAClass ref))
 
 let check_arity = function
diff --git a/toplevel/command.ml b/toplevel/command.ml
index b9a47781..3da1c838 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: command.ml,v 1.116.2.1 2004/07/16 19:31:47 herbelin Exp $ *)
+(* $Id: command.ml,v 1.116.2.3 2004/12/31 12:01:16 herbelin Exp $ *)
 
 open Pp
 open Util
@@ -49,12 +49,12 @@ let rec abstract_rawconstr c = function
       List.fold_right (fun x b -> mkLambdaC([x],t,b)) idl
         (abstract_rawconstr c bl)
 
-let rec prod_rawconstr c = function
+let rec generalize_rawconstr c = function
   | [] -> c
-  | LocalRawDef (x,b)::bl -> mkLetInC(x,b,prod_rawconstr c bl)
+  | LocalRawDef (x,b)::bl -> mkLetInC(x,b,generalize_rawconstr c bl)
   | LocalRawAssum (idl,t)::bl ->
       List.fold_right (fun x b -> mkProdC([x],t,b)) idl
-        (prod_rawconstr c bl)
+        (generalize_rawconstr c bl)
 
 let rec destSubCast c = match kind_of_term c with
   | Lambda (x,t,c) -> 
@@ -103,12 +103,28 @@ let constant_entry_of_com (bl,com,comtypopt,opacity) =
 	  const_entry_type = Some typ;
           const_entry_opaque = opacity }
 
-let red_constant_entry ce = function
+let rec length_of_raw_binders = function
+  | [] -> 0
+  | LocalRawDef _::bl -> 1 + length_of_raw_binders bl
+  | LocalRawAssum (idl,_)::bl -> List.length idl + length_of_raw_binders bl
+
+let rec under_binders env f n c =
+  if n = 0 then f env Evd.empty c else
+    match kind_of_term c with
+      | Lambda (x,t,c) ->
+        mkLambda (x,t,under_binders (push_rel (x,None,t) env) f (n-1) c)
+      | LetIn (x,b,t,c) ->
+        mkLetIn (x,b,t,under_binders (push_rel (x,Some b,t) env) f (n-1) c)
+      | _ -> assert false
+
+let red_constant_entry bl ce = function
   | None -> ce
   | Some red ->
       let body = ce.const_entry_body in
       { ce with const_entry_body = 
-	  reduction_of_redexp red (Global.env()) Evd.empty body }
+      under_binders (Global.env()) (reduction_of_redexp red)
+        (length_of_raw_binders bl)
+        body }
 
 let declare_global_definition ident ce local =
   let (_,kn) = declare_constant ident (DefinitionEntry ce,IsDefinition) in
@@ -119,9 +135,7 @@ let declare_global_definition ident ce local =
 
 let declare_definition ident (local,_) bl red_option c typopt hook =
   let ce = constant_entry_of_com (bl,c,typopt,false) in
-  if bl<>[] && red_option <> None then 
-    error "Evaluation under a local context not supported";
-  let ce' = red_constant_entry ce red_option in
+  let ce' = red_constant_entry bl ce red_option in
   let r = match local with
     | Local when Lib.sections_are_opened () ->
         let c =
@@ -168,7 +182,7 @@ let declare_one_assumption is_coe (local,kind) c (_,ident) =
   if is_coe then Class.try_add_new_coercion r local
 
 let declare_assumption idl is_coe k bl c =
-  let c = prod_rawconstr c bl in
+  let c = generalize_rawconstr c bl in
   let c = interp_type Evd.empty (Global.env()) c in
   List.iter (declare_one_assumption is_coe k c) idl
 
@@ -458,7 +472,7 @@ let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list)  =
   let (rec_sign,rec_impls,arityl) = 
     List.fold_left 
       (fun (env,impls,arl) ((recname,_,bl,arityc,_),_) -> 
-        let arityc = prod_rawconstr arityc bl in
+        let arityc = generalize_rawconstr arityc bl in
         let arity = interp_type sigma env0 arityc in
 	let impl = 
 	  if Impargs.is_implicit_args()
@@ -479,7 +493,7 @@ let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list)  =
     let def = 
       try
 	List.iter (fun (df,c,scope) -> (* No scope for tmp notation *)
-	  Metasyntax.add_notation_interpretation df [] c None) notations;
+	 Metasyntax.add_notation_interpretation df rec_impls c None) notations;
 	List.map2
 	  (fun ((_,_,bl,_,def),_) arity ->
             let def = abstract_rawconstr def bl in
@@ -533,7 +547,7 @@ let build_corecursive lnameardef =
     try 
       List.fold_left 
         (fun (env,arl) (recname,bl,arityc,_) -> 
-           let arityc = prod_rawconstr arityc bl in
+           let arityc = generalize_rawconstr arityc bl in
            let arj = type_judgment_of_rawconstr Evd.empty env0 arityc in
 	   let arity = arj.utj_val in
            let _ = declare_variable recname
@@ -546,7 +560,7 @@ let build_corecursive lnameardef =
   let recdef =
     try 
       List.map (fun (_,bl,arityc,def) ->
-        let arityc = prod_rawconstr arityc bl in
+        let arityc = generalize_rawconstr arityc bl in
         let def = abstract_rawconstr def bl in
 	let arity = interp_constr sigma rec_sign arityc in
                   interp_casted_constr sigma rec_sign def arity)
@@ -610,13 +624,6 @@ let build_scheme lnamedepindsort =
   let lrecref = List.fold_right2 declare listdecl lrecnames [] in
   if_verbose ppnl (recursive_message (Array.of_list lrecref))
 
-let rec generalize_rawconstr c = function
-  | [] -> c
-  | LocalRawDef (id,b)::bl -> mkLetInC(id,b,generalize_rawconstr c bl)
-  | LocalRawAssum (idl,t)::bl ->
-      List.fold_right (fun x b -> mkProdC([x],t,b)) idl
-        (generalize_rawconstr c bl)
-
 let start_proof id kind c hook =
   let sign = Global.named_context () in
   let sign = clear_proofs sign in
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index aa765b16..83d240a1 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coqtop.ml,v 1.72.2.3 2004/07/16 19:31:47 herbelin Exp $ *)
+(* $Id: coqtop.ml,v 1.72.2.4 2004/09/03 15:05:23 herbelin Exp $ *)
 
 open Pp
 open Util
@@ -68,7 +68,7 @@ let set_outputstate s = outputstate:=s
 let outputstate () = if !outputstate <> "" then extern_state !outputstate
 
 let check_coq_overwriting p = 
-  if string_of_id (List.hd (repr_dirpath p)) = "Coq" then
+  if string_of_id (list_last (repr_dirpath p)) = "Coq" then
     error "The \"Coq\" logical root directory is reserved for the Coq library"
 
 let set_include d p = push_include (d,p)
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index de341bd9..beb80d03 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: himsg.ml,v 1.86.2.2 2004/07/16 19:31:49 herbelin Exp $ *)
+(* $Id: himsg.ml,v 1.86.2.4 2004/12/03 18:45:53 herbelin Exp $ *)
 
 open Pp
 open Util
@@ -73,12 +73,16 @@ let explain_reference_variables c =
   str "the constant" ++ spc () ++ pc ++ spc () ++ 
   str "refers to variables which are not in the context"
 
+let rec pr_disjunction pr = function
+  | [a] -> pr  a
+  | [a;b] -> pr a ++ str " or" ++ spc () ++ pr b
+  | a::l -> pr a ++ str "," ++ spc () ++ pr_disjunction pr l
+  | [] -> assert false
+
 let explain_elim_arity ctx ind aritylst c pj okinds = 
   let ctx = make_all_name_different ctx in
   let pi = pr_inductive ctx ind in
-  let ppar = prlist_with_sep pr_coma (prterm_env ctx) aritylst in
   let pc = prterm_env ctx c in
-  let pp = prterm_env ctx pj.uj_val in
   let ppt = prterm_env ctx pj.uj_type in
   let msg = match okinds with
   | Some(kp,ki,explanation) ->
@@ -86,26 +90,41 @@ let explain_elim_arity ctx ind aritylst c pj okinds =
       let pkp = prterm_env ctx kp in
       let explanation =	match explanation with
 	| NonInformativeToInformative ->
-	  "non-informative objects may not construct informative ones."
+          "proofs can be eliminated only to build proofs"
 	| StrongEliminationOnNonSmallType ->
           "strong elimination on non-small inductive types leads to paradoxes."
 	| WrongArity ->
 	  "wrong arity" in
 	(hov 0 
-           (fnl () ++ str "Elimination of an inductive object of sort : " ++
+           (fnl () ++ str "Elimination of an inductive object of sort " ++
             pki ++ brk(1,0) ++
-            str "is not allowed on a predicate in sort : " ++ pkp  ++fnl () ++
+            str "is not allowed on a predicate in sort " ++ pkp  ++fnl () ++
             str "because" ++ spc () ++ str explanation))
   | None -> 
       mt ()
   in
-  str "Incorrect elimination of" ++ brk(1,1) ++ pc ++ spc () ++
-  str "in the inductive type" ++ brk(1,1) ++ pi ++ fnl () ++
-  str "The elimination predicate" ++ brk(1,1) ++ pp ++ spc () ++
-  str "has type" ++ brk(1,1) ++ ppt ++ fnl () ++
-  str "It should be one of :" ++ brk(1,1)  ++ hov 0 ppar ++ fnl () ++
-  msg
-
+  hov 0 (
+  str "Incorrect elimination of" ++ spc() ++ pc ++ spc () ++
+  str "in the inductive type " ++ spc() ++ quote pi ++ 
+  (if !Options.v7 then 
+    let pp = prterm_env ctx pj.uj_val in
+    let ppar = pr_disjunction (prterm_env ctx) aritylst in
+    let ppt = prterm_env ctx pj.uj_type in
+    fnl () ++
+    str "The elimination predicate"  ++ brk(1,1) ++ pp ++ spc () ++
+    str "has arity" ++ brk(1,1) ++ ppt ++ fnl () ++
+    str "It should be " ++ brk(1,1)  ++ ppar
+  else
+    let sorts = List.map (fun x -> mkSort (new_sort_in_family x))
+      (list_uniquize (List.map (fun ar ->
+      family_of_sort (destSort (snd (decompose_prod_assum ar)))) aritylst)) in
+    let ppar = pr_disjunction (prterm_env ctx) sorts in
+    let ppt = prterm_env ctx (snd (decompose_prod_assum pj.uj_type)) in
+    str "," ++ spc() ++ str "the return type has sort" ++ spc() ++ ppt ++ 
+    spc () ++ str "while it should be " ++ ppar))
+  ++ fnl () ++ msg
+    
+    
 let explain_case_not_inductive ctx cj =
   let ctx = make_all_name_different ctx in
   let pc = prterm_env ctx cj.uj_val in
@@ -322,13 +341,12 @@ let explain_hole_kind env = function
       str "a type for " ++ Nameops.pr_id id
   | BinderType Anonymous ->
       str "a type for this anonymous binder"
-  | ImplicitArg (c,n) ->
+  | ImplicitArg (c,(n,ido)) ->
       if !Options.v7 then
 	str "the " ++ pr_ord n ++
 	str " implicit argument of " ++ Nametab.pr_global_env Idset.empty c
       else
-	let imps = Impargs.implicits_of_global c in
-	let id = Impargs.name_of_implicit (List.nth imps (n-1)) in
+	let id = out_some ido in
 	str "an instance for the implicit parameter " ++
 	pr_id id ++ spc () ++ str "of" ++
 	spc () ++ Nametab.pr_global_env Idset.empty c
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 84bda0af..ca64cda0 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: metasyntax.ml,v 1.105.2.2 2004/07/16 19:31:49 herbelin Exp $ *)
+(* $Id: metasyntax.ml,v 1.105.2.6 2004/11/22 12:41:38 herbelin Exp $ *)
 
 open Pp
 open Util
@@ -606,6 +606,41 @@ let make_hunks etyps symbols from =
 
   in make NoBreak symbols
 
+let error_format () = error "The format does not match the notation"
+
+let rec split_format_at_ldots hd = function
+  | UnpTerminal s :: fmt when id_of_string s = ldots_var -> List.rev hd, fmt
+  | u :: fmt -> 
+      check_no_ldots_in_box u;
+      split_format_at_ldots (u::hd) fmt
+  | [] -> raise Exit
+
+and check_no_ldots_in_box = function
+  | UnpBox (_,fmt) ->
+      (try 
+        let _ = split_format_at_ldots [] fmt in
+        error ("The special symbol \"..\" must occur at the same formatting depth than the variables of which it is the ellipse")
+      with Exit -> ())
+  | _ -> ()
+
+let skip_var_in_recursive_format = function
+  | UnpTerminal _ :: sl (* skip first var *) ->
+      (* To do, though not so important: check that the names match
+         the names in the notation *)
+      sl
+  | _ -> error_format ()
+
+let read_recursive_format sl fmt =
+  let get_head fmt =
+    let sl = skip_var_in_recursive_format fmt in
+    try split_format_at_ldots [] sl with Exit -> error_format () in
+  let rec get_tail = function
+    | a :: sepfmt, b :: fmt when a = b -> get_tail (sepfmt, fmt)
+    | [], tail -> skip_var_in_recursive_format tail
+    | _ -> error "The format is not the same on the right and left hand side of the special token \"..\"" in
+  let slfmt, fmt = get_head fmt in
+  slfmt, get_tail (slfmt, fmt)
+
 let hunks_of_format (from,(vars,typs) as vt) symfmt = 
   let rec aux = function
   | symbs, (UnpTerminal s' as u) :: fmt
@@ -624,12 +659,20 @@ let hunks_of_format (from,(vars,typs) as vt) symfmt =
       symbs', UnpBox (a,b') :: l
   | symbs, (UnpCut _ as u) :: fmt ->
       let symbs, l = aux (symbs,fmt) in symbs, u :: l
+  | SProdList (m,sl) :: symbs, fmt ->
+      let i = list_index m vars in
+      let _,prec = precedence_of_entry_type from (List.nth typs (i-1)) in
+      let slfmt,fmt = read_recursive_format sl fmt in
+      let sl, slfmt = aux (sl,slfmt) in
+      if sl <> [] then error_format ();
+      let symbs, l = aux (symbs,fmt) in
+      symbs, UnpListMetaVar (i,prec,slfmt) :: l
   | symbs, [] -> symbs, []
-  | _, _ -> error "The format does not match the notation"
+  | _, _ -> error_format ()
   in
   match aux symfmt with
   | [], l -> l
-  | _ -> error "The format does not match the notation"
+  | _ -> error_format ()
 
 let string_of_prec (n,p) =
   (string_of_int n)^(match p with E -> "E" | L -> "L" | _ -> "")
@@ -708,13 +751,6 @@ let recompute_assoc typs =
     | _, Some Gramext.RightA -> Some Gramext.RightA
     | _ -> None
 
-let rec expand_squash = function
-  | Term ("","{") :: NonTerm (ETConstr _, n) :: Term ("","}") :: l ->
-      NonTerm (ETConstr (NextLevel,InternalProd),n)
-      :: expand_squash l
-  | a :: l -> a :: expand_squash l
-  | [] -> []
-
 let make_grammar_rule n typs symbols ntn perm =
   let assoc = recompute_assoc typs in
   let prod = make_production typs symbols in
@@ -777,7 +813,7 @@ let pr_level ntn (from,args) =
   str "at level " ++ int from ++ spc () ++ str "with arguments" ++ spc() ++
   prlist_with_sep pr_coma (pr_arg_level from) args
 
-let cache_syntax_extension (_,(_,(prec,prec8),ntn,gr,se)) =
+let cache_syntax_extension (_,(_,((prec,prec8),ntn,gr,se))) =
   try 
     let oldprec, oldprec8 = Symbols.level_of_notation ntn in
     if prec8 <> oldprec8 & (Options.do_translate () or not !Options.v7) then
@@ -799,13 +835,14 @@ let cache_syntax_extension (_,(_,(prec,prec8),ntn,gr,se)) =
 	  warning ("Notation "^ntn^
 	  " was already assigned a different level or sublevels");
       if oldprec = None or out_some oldprec <> out_some prec then
-        Egrammar.extend_grammar (Egrammar.Notation (out_some gr))
+        Egrammar.extend_grammar (Egrammar.Notation (out_some prec,out_some gr))
     end
   with Not_found ->
     (* Reserve the notation level *)
     Symbols.declare_notation_level ntn (prec,prec8);
     (* Declare the parsing rule *)
-    option_iter (fun gr -> Egrammar.extend_grammar (Egrammar.Notation gr)) gr;
+    option_iter (fun gr -> 
+      Egrammar.extend_grammar (Egrammar.Notation (out_some prec,gr))) gr;
     (* Declare the printing rule *)
     Symbols.declare_notation_printing_rule ntn (se,fst prec8)
 
@@ -813,15 +850,15 @@ let subst_notation_grammar subst x = x
 
 let subst_printing_rule subst x = x
 
-let subst_syntax_extension (_,subst,(local,prec,ntn,gr,se)) =
-  (local,prec,ntn,
+let subst_syntax_extension (_,subst,(local,(prec,ntn,gr,se))) =
+  (local,(prec,ntn,
    option_app (subst_notation_grammar subst) gr,
-   subst_printing_rule subst se)
+   subst_printing_rule subst se))
 
-let classify_syntax_definition (_,(local,_,_,_,_ as o)) =
+let classify_syntax_definition (_,(local,_ as o)) =
   if local then Dispose else Substitute o
 
-let export_syntax_definition (local,_,_,_,_ as o) =
+let export_syntax_definition (local,_ as o) =
   if local then None else Some o
 
 let (inSyntaxExtension, outSyntaxExtension) =
@@ -897,6 +934,10 @@ let check_rule_reversibility l =
   if List.for_all (function NonTerminal _ -> true | _ -> false) l then
     error "A notation must include at least one symbol"
 
+let is_not_printable = function
+  | AVar _ -> warning "This notation won't be used for printing as it is bound to a \nsingle variable"; true
+  | _ -> false
+
 let find_precedence_v7 lev etyps symbols =
   (match symbols with
     | NonTerminal x :: _ ->
@@ -1010,7 +1051,7 @@ let add_syntax_extension local mv mv8 =
     let ntn' = match data with Some ((_,_,_,_,ntn),_,_,_) -> ntn | _ -> ntn in
     let pp_rule = make_pp_rule ppdata in
     Lib.add_anonymous_leaf
-      (inSyntaxExtension (local,(prec,ppprec),ntn',gram_rule,pp_rule))
+      (inSyntaxExtension (local,((prec,ppprec),ntn',gram_rule,pp_rule)))
 	
 (**********************************************************************)
 (* Distfix, Infix, Symbols *)
@@ -1139,33 +1180,38 @@ let add_notation_in_scope local df c mods omodv8 scope toks =
   let gram_rule = make_grammar_rule n typs symbols ntn permut in
   Lib.add_anonymous_leaf
     (inSyntaxExtension
-      (local,(Some prec,ppprec),ntn,Some gram_rule,pp_rule));
+      (local,((Some prec,ppprec),ntn,Some gram_rule,pp_rule)));
 
   (* Declare interpretation *)
   let (acvars,ac) = interp_aconstr [] ppvars c in
   let a = (remove_vars pprecvars acvars,ac) (* For recursive parts *) in
   let old_pp_rule =
     (* Used only by v7; disable if contains a recursive pattern *)
-    if onlyparse or pprecvars <> [] then None
+    if onlyparse or pprecvars <> [] or not (!Options.v7) then None
     else
       let r = interp_global_rawconstr_with_vars vars c in
       Some (make_old_pp_rule n symbols typs r intnot scope vars) in
-  let onlyparse = onlyparse or !Options.v7_only in
+  let onlyparse = onlyparse or !Options.v7_only or is_not_printable ac in
   Lib.add_anonymous_leaf
     (inNotation(local,old_pp_rule,intnot,scope,a,onlyparse,false,df'))
 
 let level_rule (n,p) = if p = E then n else max (n-1) 0
 
-let check_notation_existence notation =
-  try
-    let a,_ = Symbols.level_of_notation (contract_notation notation) in
-    if a = None then raise Not_found
-  with Not_found ->
-    error "Parsing rule for this notation has to be previously declared"
+let recover_syntax ntn = 
+  try 
+    match Symbols.level_of_notation ntn with
+      | (Some prec,_ as pprec) -> 
+	  let rule,_ = Symbols.find_notation_printing_rule ntn in
+	  let gr = Egrammar.recover_notation_grammar ntn prec in
+	  Some (pprec,ntn,Some gr,rule)
+      | None,_ -> None
+  with Not_found -> None
 
-let exists_notation_syntax ntn =
-  try fst (Symbols.level_of_notation (contract_notation ntn)) <> None
-  with Not_found -> false
+let recover_notation_syntax rawntn =
+  let ntn = contract_notation rawntn in
+  match recover_syntax ntn with
+    | None -> None
+    | Some gr -> Some (gr,if ntn=rawntn then None else recover_syntax "{ _ }")
 
 let set_data_for_v7_pp recs a vars =
   if not !Options.v7 then None else
@@ -1185,34 +1231,44 @@ let build_old_pp_rule notation scope symbs (r,vars) =
   make_old_pp_rule (fst prec) symbs typs r notation scope vars
 
 let add_notation_interpretation_core local symbs for_old df a scope onlyparse 
-  onlypp =
+  onlypp gram_data =
   let notation = make_notation_key symbs in
   let old_pp_rule = 
     if !Options.v7 then 
       option_app (build_old_pp_rule notation scope symbs) for_old
     else None in
+  option_iter
+    (fun (x,y) ->
+      Lib.add_anonymous_leaf (inSyntaxExtension (local,x));
+      option_iter
+	(fun z -> Lib.add_anonymous_leaf (inSyntaxExtension (local,z))) y)
+    gram_data;
   Lib.add_anonymous_leaf
     (inNotation(local,old_pp_rule,notation,scope,a,onlyparse,onlypp,
      (Lib.library_dp(),df)))
 
 let add_notation_interpretation df names c sc =
   let (recs,vars,symbs) = analyse_notation_tokens (split_notation_string df) in
-  check_notation_existence (make_notation_key symbs);
+  let gram_data = recover_notation_syntax (make_notation_key symbs) in
+  if gram_data = None then
+    error "Parsing rule for this notation has to be previously declared";
   let (acvars,ac) = interp_aconstr names vars c in
   let a = (remove_vars recs acvars,ac) (* For recursive parts *) in
   let a_for_old = interp_rawconstr_with_implicits Evd.empty (Global.env()) vars names c in
   let for_oldpp = set_data_for_v7_pp recs a_for_old vars in
-  add_notation_interpretation_core false symbs for_oldpp df a sc false false
+  let onlyparse = is_not_printable ac in
+  add_notation_interpretation_core false symbs for_oldpp df a sc onlyparse 
+    false gram_data
 
 let add_notation_in_scope_v8only local df c mv8 scope toks =
   let (_,recs,vars,intnot,notation),prec,ppdata,df' = compute_syntax_data false (df,mv8) in
   let pp_rule = make_pp_rule ppdata in
   Lib.add_anonymous_leaf
-    (inSyntaxExtension(local,(None,prec),notation,None,pp_rule));
+    (inSyntaxExtension(local,((None,prec),notation,None,pp_rule)));
   (* Declare the interpretation *)
-  let onlyparse = false in
   let (acvars,ac) = interp_aconstr [] vars c in
   let a = (remove_vars recs acvars,ac) (* For recursive parts *) in
+  let onlyparse = is_not_printable ac in
   Lib.add_anonymous_leaf
     (inNotation(local,None,intnot,scope,a,onlyparse,true,df'))
 
@@ -1231,11 +1287,12 @@ let add_notation_v8only local c (df,modifiers) sc =
 	      else
 	        (* Declare only interpretation *)
 		let (recs,vars,symbs) = analyse_notation_tokens toks in
-		let onlyparse = modifiers = [SetOnlyParsing] in
                 let (acvars,ac) = interp_aconstr [] vars c in
+		let onlyparse = modifiers = [SetOnlyParsing] 
+                  or is_not_printable ac in
                 let a = (remove_vars recs acvars,ac) in
 		add_notation_interpretation_core local symbs None df a sc 
-		  onlyparse true
+		  onlyparse true None
 	  | Some n ->
 	    (* Declare both syntax and interpretation *)
 	      let mods =
@@ -1266,14 +1323,17 @@ let add_notation local c dfmod mv8 sc =
 	      else
 	        (* Declare only interpretation *)
 		let (recs,vars,symbs) = analyse_notation_tokens toks in
-                if exists_notation_syntax (make_notation_key symbs) then
-		  let onlyparse = modifiers = [SetOnlyParsing] in
+                let gram_data =
+		  recover_notation_syntax (make_notation_key symbs) in
+		if gram_data <> None then
                   let (acvars,ac) = interp_aconstr [] vars c in
                   let a = (remove_vars recs acvars,ac) in
+		  let onlyparse = modifiers = [SetOnlyParsing] 
+                    or is_not_printable ac in
 		  let a_for_old = interp_global_rawconstr_with_vars vars c in
                   let for_old = set_data_for_v7_pp recs a_for_old vars in
 		  add_notation_interpretation_core local symbs for_old df a
-		    sc onlyparse false
+		    sc onlyparse false gram_data
                 else
                   add_notation_in_scope local df c modifiers mv8 sc toks
 	  | Some n ->
@@ -1340,7 +1400,7 @@ let add_infix local (inf,modl) pr mv8 sc =
       let a' = (remove_vars recs acvars,ac) in
       let a_for_old = interp_global_rawconstr_with_vars vars a in
       add_notation_interpretation_core local symbs None df a' sc 
-	onlyparse true
+	onlyparse true None
     else
       if n8 = None then error "Needs a level" else
       let mv8 = match a8 with None -> SetAssoc Gramext.NonA :: mv8 |_ -> mv8 in
@@ -1365,13 +1425,14 @@ let add_infix local (inf,modl) pr mv8 sc =
     (* de ne déclarer que l'interprétation *)
     (* Declare only interpretation *)
     let (recs,vars,symbs) = analyse_notation_tokens toks in
-    if exists_notation_syntax (make_notation_key symbs) then
+    let gram_data = recover_notation_syntax (make_notation_key symbs) in
+    if gram_data <> None then 
       let (acvars,ac) = interp_aconstr [] vars a in
       let a' = (remove_vars recs acvars,ac) in
       let a_for_old = interp_global_rawconstr_with_vars vars a in
       let for_old = set_data_for_v7_pp recs a_for_old vars in
       add_notation_interpretation_core local symbs for_old df a' sc 
-        onlyparse false
+        onlyparse false gram_data
     else
       let mv,mv8 = make_infix_data n assoc modl mv8 in
       add_notation_in_scope local df a mv mv8 sc toks
diff --git a/toplevel/recordobj.mli b/toplevel/recordobj.mli
index 8ea39767..91550c34 100755
--- a/toplevel/recordobj.mli
+++ b/toplevel/recordobj.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: recordobj.mli,v 1.7.6.1 2004/07/16 19:31:49 herbelin Exp $ *)
+(*i $Id: recordobj.mli,v 1.7.6.2 2005/01/21 17:18:33 herbelin Exp $ i*)
 
 val objdef_declare : Libnames.global_reference -> unit
 val add_object_hook : Tacexpr.declaration_hook
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 9fe8b280..b00cfffc 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: usage.ml,v 1.15.2.1 2004/07/16 19:31:50 herbelin Exp $ *)
+(* $Id: usage.ml,v 1.15.2.2 2004/09/03 14:35:26 herbelin Exp $ *)
 
 let version () =
   Printf.printf "The Coq Proof Assistant, version %s (%s)\n"
@@ -23,7 +23,7 @@ let print_usage_channel co command =
 "  -I dir                 add directory dir in the include path
   -include dir           (idem)
   -R dir coqdir          recursively map physical dir to logical coqdir 
-  -src                   add source directories in the include path
+  -top coqdir            set the toplevel name to be coqdir instead of Top
 
   -inputstate f          read state from file f.coq
   -is f                  (idem)
@@ -35,14 +35,14 @@ let print_usage_channel co command =
   -load-vernac-source f  load Coq file f.v (Load f.)
   -l f                   (idem) 
   -load-vernac-source-verbose f  load Coq file f.v (Load Verbose f.)
-  -lv f			(idem)
+  -lv f	                 (idem)
   -load-vernac-object f  load Coq object file f.vo
   -require f             load Coq object file f.vo and import it (Require f.)
   -compile f             compile Coq file f.v (implies -batch)
   -compile-verbose f     verbosely compile Coq file f.v (implies -batch)
 
-  -opt                   run the native-code version of Coq or Coq_SearchIsos
-  -byte                  run the bytecode version of Coq or Coq_SearchIsos
+  -opt                   run the native-code version of Coq
+  -byte                  run the bytecode version of Coq
 
   -where                 print Coq's standard library location and exit
   -v                     print Coq version and exit
@@ -59,6 +59,9 @@ let print_usage_channel co command =
   -xml                   export XML files either to the hierarchy rooted in
                          the directory $COQ_XML_LIBRARY_ROOT (if set) or to
                          stdout (if unset)
+  -quality               improve the legibility of the proof terms produced by
+                         some tactics
+  -h, --help             print this list of options
 "
 
 (* print the usage on standard error *)
@@ -72,5 +75,6 @@ let print_usage_coqc () =
   print_usage "Usage: coqc <options> <Coq options> file...\n
 options are:
   -verbose  compile verbosely
+  -bindir   override the default directory where coqc looks for coqtop
   -image f  specify an alternative executable for Coq
   -t        keep temporary files\n\n"
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index a359b4a1..89e0d708 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: vernacentries.mli,v 1.16.2.1 2004/07/16 19:31:50 herbelin Exp $ i*)
+(*i $Id: vernacentries.mli,v 1.16.2.2 2005/01/21 16:41:52 herbelin Exp $ i*)
 
 (*i*)
 open Names
@@ -27,11 +27,11 @@ val show_node : unit -> unit
    in the context of the current goal, as for instance in pcoq *)
 val get_current_context_of_args : int option -> Evd.evar_map * Environ.env
 
+(*i
 (* this function is used to analyse the extra arguments in search commands.
    It is used in pcoq. *) (*i anciennement: inside_outside i*)
-(*
 val interp_search_restriction : search_restriction -> dir_path list * bool
-*)
+i*)
 
 type pcoq_hook = {
   start_proof : unit -> unit;
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index e1525c17..382434dc 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: vernacexpr.ml,v 1.55.2.1 2004/07/16 19:31:50 herbelin Exp $ *)
+(*i $Id: vernacexpr.ml,v 1.55.2.2 2005/01/21 17:14:10 herbelin Exp $ i*)
 
 open Util
 open Names