bug make_strength repare

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

8 files changed, 94 insertions, 61 deletions

diff --git a/.depend b/.depend
index 978f5368c..547c304d0 100644
--- a/.depend
+++ b/.depend
@@ -100,8 +100,8 @@ pretyping/syntax_def.cmi: kernel/names.cmi pretyping/rawterm.cmi
 pretyping/tacred.cmi: kernel/closure.cmi kernel/environ.cmi kernel/evd.cmi \
     kernel/names.cmi kernel/reduction.cmi kernel/term.cmi 
 pretyping/typing.cmi: kernel/environ.cmi kernel/evd.cmi kernel/term.cmi 
-proofs/clenv.cmi: kernel/names.cmi proofs/proof_trees.cmi proofs/tacmach.cmi \
-    kernel/term.cmi lib/util.cmi 
+proofs/clenv.cmi: kernel/names.cmi lib/pp.cmi proofs/proof_trees.cmi \
+    proofs/tacmach.cmi kernel/term.cmi lib/util.cmi 
 proofs/evar_refiner.cmi: kernel/environ.cmi kernel/evd.cmi kernel/names.cmi \
     proofs/proof_trees.cmi proofs/refiner.cmi kernel/sign.cmi kernel/term.cmi 
 proofs/logic.cmi: kernel/environ.cmi kernel/evd.cmi kernel/names.cmi \
@@ -172,6 +172,36 @@ config/coq_config.cmo: config/coq_config.cmi
 config/coq_config.cmx: config/coq_config.cmi 
 dev/db_printers.cmo: kernel/names.cmi lib/pp.cmi 
 dev/db_printers.cmx: kernel/names.cmx lib/pp.cmx 
+dev/top_printers.cmo: parsing/ast.cmi parsing/astterm.cmi proofs/clenv.cmi \
+    kernel/closure.cmi toplevel/command.cmi kernel/constant.cmi \
+    parsing/coqast.cmi library/discharge.cmi parsing/egrammar.cmi \
+    tactics/elim.cmi kernel/environ.cmi parsing/esyntax.cmi kernel/evd.cmi \
+    kernel/generic.cmi kernel/inductive.cmi parsing/lexer.cmi \
+    library/libobject.cmi library/library.cmi toplevel/metasyntax.cmi \
+    toplevel/mltop.cmi kernel/names.cmi proofs/pfedit.cmi lib/pp.cmi \
+    parsing/pretty.cmi parsing/printer.cmi proofs/proof_trees.cmi \
+    kernel/reduction.cmi proofs/refiner.cmi kernel/sign.cmi kernel/sosub.cmi \
+    library/states.cmi library/summary.cmi lib/system.cmi \
+    tactics/tacentries.cmi proofs/tacinterp.cmi proofs/tacmach.cmi \
+    tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \
+    parsing/termast.cmi toplevel/toplevel.cmi pretyping/typing.cmi \
+    kernel/univ.cmi toplevel/vernac.cmi toplevel/vernacentries.cmi \
+    toplevel/vernacinterp.cmi 
+dev/top_printers.cmx: parsing/ast.cmx parsing/astterm.cmx proofs/clenv.cmx \
+    kernel/closure.cmx toplevel/command.cmx kernel/constant.cmx \
+    parsing/coqast.cmx library/discharge.cmx parsing/egrammar.cmx \
+    tactics/elim.cmx kernel/environ.cmx parsing/esyntax.cmx kernel/evd.cmx \
+    kernel/generic.cmx kernel/inductive.cmx parsing/lexer.cmx \
+    library/libobject.cmx library/library.cmx toplevel/metasyntax.cmx \
+    toplevel/mltop.cmx kernel/names.cmx proofs/pfedit.cmx lib/pp.cmx \
+    parsing/pretty.cmx parsing/printer.cmx proofs/proof_trees.cmx \
+    kernel/reduction.cmx proofs/refiner.cmx kernel/sign.cmx kernel/sosub.cmx \
+    library/states.cmx library/summary.cmx lib/system.cmx \
+    tactics/tacentries.cmx proofs/tacinterp.cmx proofs/tacmach.cmx \
+    tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \
+    parsing/termast.cmx toplevel/toplevel.cmx pretyping/typing.cmx \
+    kernel/univ.cmx toplevel/vernac.cmx toplevel/vernacentries.cmx \
+    toplevel/vernacinterp.cmx 
 kernel/abstraction.cmo: kernel/generic.cmi kernel/names.cmi kernel/sosub.cmi \
     kernel/term.cmi lib/util.cmi kernel/abstraction.cmi 
 kernel/abstraction.cmx: kernel/generic.cmx kernel/names.cmx kernel/sosub.cmx \
@@ -376,22 +406,20 @@ parsing/ast.cmo: parsing/coqast.cmi lib/dyn.cmi lib/hashcons.cmi \
     kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi lib/util.cmi parsing/ast.cmi 
 parsing/ast.cmx: parsing/coqast.cmx lib/dyn.cmx lib/hashcons.cmx \
     kernel/names.cmx parsing/pcoq.cmi lib/pp.cmx lib/util.cmx parsing/ast.cmi 
-parsing/astterm.cmo: parsing/ast.cmi kernel/closure.cmi toplevel/command.cmi \
-    parsing/coqast.cmi library/declare.cmi kernel/environ.cmi \
-    pretyping/evarutil.cmi kernel/evd.cmi kernel/generic.cmi \
-    library/global.cmi library/impargs.cmi kernel/names.cmi \
-    library/nametab.cmi parsing/pcoq.cmi lib/pp.cmi pretyping/pretyping.cmi \
-    pretyping/rawterm.cmi kernel/reduction.cmi kernel/sign.cmi \
-    pretyping/syntax_def.cmi pretyping/tacred.cmi kernel/term.cmi \
-    pretyping/typing.cmi lib/util.cmi toplevel/vernac.cmi parsing/astterm.cmi 
-parsing/astterm.cmx: parsing/ast.cmx kernel/closure.cmx toplevel/command.cmx \
-    parsing/coqast.cmx library/declare.cmx kernel/environ.cmx \
-    pretyping/evarutil.cmx kernel/evd.cmx kernel/generic.cmx \
-    library/global.cmx library/impargs.cmx kernel/names.cmx \
-    library/nametab.cmx parsing/pcoq.cmi lib/pp.cmx pretyping/pretyping.cmx \
-    pretyping/rawterm.cmi kernel/reduction.cmx kernel/sign.cmx \
-    pretyping/syntax_def.cmx pretyping/tacred.cmx kernel/term.cmx \
-    pretyping/typing.cmx lib/util.cmx toplevel/vernac.cmx parsing/astterm.cmi 
+parsing/astterm.cmo: parsing/ast.cmi kernel/closure.cmi parsing/coqast.cmi \
+    library/declare.cmi kernel/environ.cmi pretyping/evarutil.cmi \
+    kernel/evd.cmi kernel/generic.cmi library/global.cmi library/impargs.cmi \
+    kernel/names.cmi library/nametab.cmi parsing/pcoq.cmi lib/pp.cmi \
+    pretyping/pretyping.cmi pretyping/rawterm.cmi kernel/reduction.cmi \
+    kernel/sign.cmi pretyping/syntax_def.cmi pretyping/tacred.cmi \
+    kernel/term.cmi pretyping/typing.cmi lib/util.cmi parsing/astterm.cmi 
+parsing/astterm.cmx: parsing/ast.cmx kernel/closure.cmx parsing/coqast.cmx \
+    library/declare.cmx kernel/environ.cmx pretyping/evarutil.cmx \
+    kernel/evd.cmx kernel/generic.cmx library/global.cmx library/impargs.cmx \
+    kernel/names.cmx library/nametab.cmx parsing/pcoq.cmi lib/pp.cmx \
+    pretyping/pretyping.cmx pretyping/rawterm.cmi kernel/reduction.cmx \
+    kernel/sign.cmx pretyping/syntax_def.cmx pretyping/tacred.cmx \
+    kernel/term.cmx pretyping/typing.cmx lib/util.cmx parsing/astterm.cmi 
 parsing/coqast.cmo: lib/dyn.cmi lib/hashcons.cmi parsing/coqast.cmi 
 parsing/coqast.cmx: lib/dyn.cmx lib/hashcons.cmx parsing/coqast.cmi 
 parsing/egrammar.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/extend.cmi \
@@ -540,12 +568,14 @@ pretyping/typing.cmx: kernel/environ.cmx kernel/generic.cmx kernel/names.cmx \
     kernel/typeops.cmx lib/util.cmx pretyping/typing.cmi 
 proofs/clenv.cmo: kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \
     kernel/instantiate.cmi proofs/logic.cmi kernel/names.cmi lib/pp.cmi \
-    proofs/proof_trees.cmi kernel/reduction.cmi kernel/sign.cmi \
-    proofs/tacmach.cmi kernel/term.cmi lib/util.cmi proofs/clenv.cmi 
+    parsing/printer.cmi proofs/proof_trees.cmi kernel/reduction.cmi \
+    kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi lib/util.cmi \
+    proofs/clenv.cmi 
 proofs/clenv.cmx: kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx \
     kernel/instantiate.cmx proofs/logic.cmx kernel/names.cmx lib/pp.cmx \
-    proofs/proof_trees.cmx kernel/reduction.cmx kernel/sign.cmx \
-    proofs/tacmach.cmx kernel/term.cmx lib/util.cmx proofs/clenv.cmi 
+    parsing/printer.cmx proofs/proof_trees.cmx kernel/reduction.cmx \
+    kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx lib/util.cmx \
+    proofs/clenv.cmi 
 proofs/evar_refiner.cmo: kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \
     proofs/logic.cmi kernel/names.cmi lib/pp.cmi proofs/proof_trees.cmi \
     kernel/reduction.cmi proofs/refiner.cmi lib/stamps.cmi kernel/term.cmi \
diff --git a/Makefile b/Makefile
index 8db9dc19e..f2c7be609 100644
--- a/Makefile
+++ b/Makefile
@@ -115,7 +115,7 @@ CMX=$(CMO:.cmo=.cmx)
 
 COQMKTOP=scripts/coqmktop
 
-world: minicoq coqtop.byte dev/db_printers.cmo
+world: minicoq coqtop.byte $(COQMKTOP) dev/db_printers.cmo
 
 coqtop: $(COQMKTOP) $(CMX)
 	$(COQMKTOP) -opt -notactics $(OPTFLAGS) -o coqtop
diff --git a/configure b/configure
index ee493b3dd..073379bbf 100755
--- a/configure
+++ b/configure
@@ -8,7 +8,7 @@
 
 VERSION=7.00
 VERSIONSI=1.0
-DATE="August 1999"
+DATE="December 1999"
 
 # a local which command for sh
 which () {
diff --git a/kernel/names.ml b/kernel/names.ml
index dd7ad6f3a..2686763aa 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -199,8 +199,8 @@ let append_to_path sp str =
   make_path sp (id_of_string ((string_of_id id)^str)) k
 
 let sp_of_wd = function
-  | bn::dp -> make_path dp (id_of_string bn) OBJ
-  | _      -> invalid_arg "Names.sp_of_wd"
+  | [] -> invalid_arg "Names.sp_of_wd"
+  | l -> let (bn,dp) = list_sep_last l in make_path dp (id_of_string bn) OBJ
 
 let wd_of_sp sp = 
   let (sp,id,_) = repr_path sp in sp @ [string_of_id id]
diff --git a/library/declare.ml b/library/declare.ml
index 91fcc7df6..1a1d46d3f 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -25,11 +25,13 @@ let make_strength = function
 let make_strength_0 () = make_strength (Lib.cwd())
 
 let make_strength_1 () =
-  let path = try List.tl (List.tl (Lib.cwd())) with Failure _ -> [] in
+  let cwd = Lib.cwd() in
+  let path = try list_firstn (List.length cwd - 1) cwd with Failure _ -> [] in
   make_strength path
 
 let make_strength_2 () =
-  let path = try List.tl (Lib.cwd()) with Failure _ -> [] in
+  let cwd = Lib.cwd() in
+  let path = try list_firstn (List.length cwd - 2) cwd with Failure _ -> [] in
   make_strength path
 
 
diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index b595c901f..7babfe020 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -428,14 +428,15 @@ let globalize_ast ast =
 
 
 (* Installation of the AST quotations. "command" is used by default. *)
-open Pcoq
-
 let _ = 
-  define_quotation true "command" (map_entry globalize_command Command.command)
+  Pcoq.define_quotation true "command" 
+    (Pcoq.map_entry globalize_command Pcoq.Command.command)
 let _ = 
-  define_quotation false "tactic" (map_entry globalize_ast Tactic.tactic)
+  Pcoq.define_quotation false "tactic" 
+    (Pcoq.map_entry globalize_ast Pcoq.Tactic.tactic)
 let _ = 
-  define_quotation false "vernac" (map_entry globalize_ast Vernac.vernac)
+  Pcoq.define_quotation false "vernac" 
+    (Pcoq.map_entry globalize_ast Pcoq.Vernac.vernac)
 
 
 (*********************************************************************)
diff --git a/parsing/lexer.mll b/parsing/lexer.mll
index 5cb993b26..adafc2c84 100644
--- a/parsing/lexer.mll
+++ b/parsing/lexer.mll
@@ -84,7 +84,7 @@ let identchar =
   ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' 
    '\'' '0'-'9']
 let symbolchar =
-  ['!' '$' '%' '&' '*' '+' '-' '<' '>' '/' ':' '=' '?' '@' '^' '|' '~' '#']
+  ['!' '$' '%' '&' '*' '+' '-' '<' '>' '/' ':' ';' '=' '?' '@' '^' '|' '~' '#']
 let decimal_literal = ['0'-'9']+
 let hex_literal = '0' ['x' 'X'] ['0'-'9' 'A'-'F' 'a'-'f']+
 let oct_literal = '0' ['o' 'O'] ['0'-'7']+
@@ -98,7 +98,7 @@ rule token = parse
 	if is_keyword s then ("",s) else ("IDENT",s) }
   | decimal_literal | hex_literal | oct_literal | bin_literal
       { ("INT", Lexing.lexeme lexbuf) }
-  | "(" | ")" | "[" | "]" | "{" | "}" | "<" | ">" | "." | "_" 
+  | "(" | ")" | "[" | "]" | "{" | "}" | "." | "_" 
       { ("", Lexing.lexeme lexbuf) }
   | symbolchar+
       { ("", Lexing.lexeme lexbuf) }
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index f6f696ea3..e3adda7f0 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -91,33 +91,33 @@ let just_parsing = ref false
 let rec vernac interpfun input =
   let com = parse_phrase input in
   let rec interp com =
-    try
-      match com with
-	| Node (_,"LoadFile",[Str(_, verbosely); Str(_,fname)]) ->
-            let verbosely = verbosely = "Verbose" in
-            raw_load_vernac_file verbosely (make_suffix fname ".v")
-              
-	| Node (_,"CompileFile",[Str(_,verbosely); Str(_,only_spec);
-				 Str (_,mname); Str(_,fname)]) ->
-            let verbosely = verbosely = "Verbose" in
-            let only_spec = only_spec = "Specification" in
-            States.with_heavy_rollback (* to roll back in case of error *)
-              (raw_compile_module verbosely only_spec mname)
-              (make_suffix fname ".v")
-	      
-	| Node(_,"Time",l) ->
-	    let tstart = System.get_time() in
-            List.iter interp l;
-	    let tend = System.get_time() in
-            mSGNL [< 'sTR"Finished transaction in " ;
-                     System.fmt_time_difference tstart tend >]
-	      
-	| _ -> if not !just_parsing then interpfun com
-    with e -> 
-      raise (DuringCommandInterp (Ast.loc com, e))
+    match com with
+      | Node (_,"LoadFile",[Str(_, verbosely); Str(_,fname)]) ->
+          let verbosely = verbosely = "Verbose" in
+          raw_load_vernac_file verbosely (make_suffix fname ".v")
+            
+      | Node (_,"CompileFile",[Str(_,verbosely); Str(_,only_spec);
+			       Str (_,mname); Str(_,fname)]) ->
+          let verbosely = verbosely = "Verbose" in
+          let only_spec = only_spec = "Specification" in
+          States.with_heavy_rollback (* to roll back in case of error *)
+            (raw_compile_module verbosely only_spec mname)
+            (make_suffix fname ".v")
+	    
+      | Node(_,"Time",l) ->
+	  let tstart = System.get_time() in
+          List.iter interp l;
+	  let tend = System.get_time() in
+          mSGNL [< 'sTR"Finished transaction in " ;
+                   System.fmt_time_difference tstart tend >]
+	    
+      | _ -> if not !just_parsing then interpfun com
   in 
-  interp com
-     
+  try
+    interp com
+  with e -> 
+    raise (DuringCommandInterp (Ast.loc com, e))
+    
 and raw_load_vernac_file verbosely s =
   let _ = read_vernac_file verbosely s in ()