poursuite de Vernacentries

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

17 files changed, 269 insertions, 101 deletions

diff --git a/.depend b/.depend
index 654c9c5f2e..31deddb792 100644
--- a/.depend
+++ b/.depend
@@ -54,6 +54,8 @@ parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \
 parsing/astterm.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \
     kernel/names.cmi pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi 
 parsing/coqast.cmi: lib/dyn.cmi 
+parsing/egrammar.cmi: parsing/ast.cmi parsing/coqast.cmi parsing/extend.cmi \
+    parsing/pcoq.cmi 
 parsing/esyntax.cmi: parsing/ast.cmi parsing/coqast.cmi parsing/extend.cmi \
     lib/pp.cmi 
 parsing/extend.cmi: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi \
@@ -98,8 +100,9 @@ proofs/logic.cmi: kernel/environ.cmi kernel/evd.cmi kernel/names.cmi \
     lib/pp.cmi proofs/proof_trees.cmi kernel/sign.cmi kernel/term.cmi 
 proofs/macros.cmi: parsing/ast.cmi parsing/coqast.cmi kernel/names.cmi \
     proofs/proof_trees.cmi proofs/tacmach.cmi 
-proofs/pfedit.cmi: library/declare.cmi lib/pp.cmi proofs/proof_trees.cmi \
-    kernel/sign.cmi proofs/tacmach.cmi 
+proofs/pfedit.cmi: parsing/coqast.cmi library/declare.cmi kernel/environ.cmi \
+    lib/pp.cmi proofs/proof_trees.cmi kernel/sign.cmi proofs/tacmach.cmi \
+    kernel/term.cmi 
 proofs/proof_trees.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \
     kernel/names.cmi lib/pp.cmi kernel/sign.cmi lib/stamps.cmi \
     kernel/term.cmi lib/util.cmi 
@@ -137,11 +140,16 @@ tactics/tactics.cmi: proofs/clenv.cmi kernel/evd.cmi kernel/names.cmi \
 tactics/termdn.cmi: tactics/dn.cmi kernel/generic.cmi kernel/term.cmi 
 tactics/wcclausenv.cmi: proofs/clenv.cmi kernel/evd.cmi kernel/names.cmi \
     proofs/proof_trees.cmi kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi 
+toplevel/command.cmi: parsing/coqast.cmi library/declare.cmi kernel/names.cmi \
+    proofs/tacred.cmi kernel/term.cmi 
 toplevel/errors.cmi: parsing/coqast.cmi lib/pp.cmi 
 toplevel/himsg.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
     kernel/sign.cmi kernel/term.cmi kernel/type_errors.cmi 
+toplevel/metasyntax.cmi: parsing/coqast.cmi parsing/extend.cmi 
 toplevel/mltop.cmi: library/libobject.cmi 
 toplevel/protectedtoplevel.cmi: lib/pp.cmi 
+toplevel/searchisos.cmi: library/libobject.cmi kernel/names.cmi \
+    kernel/term.cmi 
 toplevel/toplevel.cmi: parsing/pcoq.cmi lib/pp.cmi 
 toplevel/vernac.cmi: parsing/coqast.cmi parsing/pcoq.cmi 
 toplevel/vernacentries.cmi: kernel/names.cmi kernel/term.cmi \
@@ -262,8 +270,8 @@ lib/gset.cmo: lib/gset.cmi
 lib/gset.cmx: lib/gset.cmi 
 lib/hashcons.cmo: lib/hashcons.cmi 
 lib/hashcons.cmx: lib/hashcons.cmi 
-lib/options.cmo: lib/options.cmi 
-lib/options.cmx: lib/options.cmi 
+lib/options.cmo: lib/util.cmi lib/options.cmi 
+lib/options.cmx: lib/util.cmx lib/options.cmi 
 lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi 
 lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi 
 lib/pp_control.cmo: lib/pp_control.cmi 
@@ -352,20 +360,28 @@ 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 parsing/coqast.cmi library/declare.cmi \
-    kernel/environ.cmi pretyping/evarutil.cmi kernel/evd.cmi \
-    kernel/generic.cmi library/global.cmi library/impargs.cmi \
+parsing/astterm.cmo: parsing/ast.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 parsing/pcoq.cmi lib/pp.cmi pretyping/pretyping.cmi \
-    pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi \
-    pretyping/typing.cmi lib/util.cmi toplevel/vernac.cmi parsing/astterm.cmi 
-parsing/astterm.cmx: parsing/ast.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 \
+    pretyping/rawterm.cmi kernel/reduction.cmi kernel/sign.cmi \
+    kernel/term.cmi pretyping/typing.cmi lib/util.cmi toplevel/vernac.cmi \
+    parsing/astterm.cmi 
+parsing/astterm.cmx: parsing/ast.cmx toplevel/command.cmi 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 parsing/pcoq.cmi lib/pp.cmx pretyping/pretyping.cmx \
-    pretyping/rawterm.cmi kernel/sign.cmx kernel/term.cmx \
-    pretyping/typing.cmx lib/util.cmx toplevel/vernac.cmx parsing/astterm.cmi 
+    pretyping/rawterm.cmi kernel/reduction.cmx kernel/sign.cmx \
+    kernel/term.cmx pretyping/typing.cmx lib/util.cmx toplevel/vernac.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 \
+    parsing/lexer.cmi parsing/pcoq.cmi lib/pp.cmi lib/util.cmi \
+    parsing/egrammar.cmi 
+parsing/egrammar.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/extend.cmi \
+    parsing/lexer.cmx parsing/pcoq.cmi lib/pp.cmx lib/util.cmx \
+    parsing/egrammar.cmi 
 parsing/esyntax.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/extend.cmi \
     lib/gmap.cmi lib/gmapl.cmi lib/pp.cmi lib/util.cmi parsing/esyntax.cmi 
 parsing/esyntax.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/extend.cmi \
@@ -512,14 +528,16 @@ proofs/macros.cmx: parsing/ast.cmx parsing/coqast.cmx library/lib.cmx \
     library/libobject.cmx library/library.cmx kernel/names.cmx \
     parsing/pcoq.cmi lib/pp.cmx proofs/proof_trees.cmx library/summary.cmx \
     kernel/term.cmx lib/util.cmx proofs/macros.cmi 
-proofs/pfedit.cmo: kernel/constant.cmi library/declare.cmi lib/edit.cmi \
-    kernel/evd.cmi kernel/generic.cmi library/global.cmi library/lib.cmi \
-    kernel/names.cmi lib/pp.cmi proofs/proof_trees.cmi kernel/sign.cmi \
-    proofs/tacmach.cmi kernel/term.cmi lib/util.cmi proofs/pfedit.cmi 
-proofs/pfedit.cmx: kernel/constant.cmx library/declare.cmx lib/edit.cmx \
-    kernel/evd.cmx kernel/generic.cmx library/global.cmx library/lib.cmx \
-    kernel/names.cmx lib/pp.cmx proofs/proof_trees.cmx kernel/sign.cmx \
-    proofs/tacmach.cmx kernel/term.cmx lib/util.cmx proofs/pfedit.cmi 
+proofs/pfedit.cmo: parsing/astterm.cmi kernel/constant.cmi \
+    library/declare.cmi lib/edit.cmi kernel/environ.cmi kernel/evd.cmi \
+    kernel/generic.cmi library/global.cmi library/lib.cmi kernel/names.cmi \
+    lib/pp.cmi proofs/proof_trees.cmi kernel/sign.cmi proofs/tacmach.cmi \
+    kernel/term.cmi pretyping/typing.cmi lib/util.cmi proofs/pfedit.cmi 
+proofs/pfedit.cmx: parsing/astterm.cmx kernel/constant.cmx \
+    library/declare.cmx lib/edit.cmx kernel/environ.cmx kernel/evd.cmx \
+    kernel/generic.cmx library/global.cmx library/lib.cmx kernel/names.cmx \
+    lib/pp.cmx proofs/proof_trees.cmx kernel/sign.cmx proofs/tacmach.cmx \
+    kernel/term.cmx pretyping/typing.cmx lib/util.cmx proofs/pfedit.cmi 
 proofs/proof_trees.cmo: parsing/ast.cmi parsing/coqast.cmi kernel/environ.cmi \
     kernel/evd.cmi kernel/names.cmi lib/pp.cmi parsing/pretty.cmi \
     parsing/printer.cmi kernel/sign.cmi lib/stamps.cmi kernel/term.cmi \
@@ -686,6 +704,14 @@ toplevel/himsg.cmo: kernel/environ.cmi kernel/generic.cmi kernel/names.cmi \
 toplevel/himsg.cmx: kernel/environ.cmx kernel/generic.cmx kernel/names.cmx \
     lib/pp.cmx kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \
     kernel/type_errors.cmx lib/util.cmx toplevel/himsg.cmi 
+toplevel/metasyntax.cmo: parsing/ast.cmi parsing/coqast.cmi \
+    parsing/egrammar.cmi parsing/esyntax.cmi parsing/extend.cmi \
+    library/lib.cmi library/libobject.cmi library/library.cmi \
+    parsing/pcoq.cmi lib/pp.cmi library/summary.cmi toplevel/metasyntax.cmi 
+toplevel/metasyntax.cmx: parsing/ast.cmx parsing/coqast.cmx \
+    parsing/egrammar.cmx parsing/esyntax.cmx parsing/extend.cmi \
+    library/lib.cmx library/libobject.cmx library/library.cmx \
+    parsing/pcoq.cmi lib/pp.cmx library/summary.cmx toplevel/metasyntax.cmi 
 toplevel/minicoq.cmo: kernel/constant.cmi parsing/g_minicoq.cmi \
     kernel/generic.cmi toplevel/himsg.cmi kernel/inductive.cmi \
     kernel/names.cmi lib/pp.cmi kernel/safe_typing.cmi kernel/sign.cmi \
@@ -722,26 +748,30 @@ toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/library.cmx \
     lib/options.cmx parsing/pcoq.cmi proofs/pfedit.cmx lib/pp.cmx \
     library/states.cmx lib/system.cmx lib/util.cmx toplevel/vernacinterp.cmx \
     toplevel/vernac.cmi 
-toplevel/vernacentries.cmo: parsing/ast.cmi pretyping/class.cmi \
-    pretyping/classops.cmi parsing/coqast.cmi library/declare.cmi \
-    kernel/environ.cmi kernel/evd.cmi parsing/extend.cmi library/global.cmi \
-    library/libobject.cmi library/library.cmi proofs/macros.cmi \
-    kernel/names.cmi library/nametab.cmi lib/options.cmi parsing/pcoq.cmi \
-    proofs/pfedit.cmi lib/pp.cmi lib/pp_control.cmi parsing/pretty.cmi \
+toplevel/vernacentries.cmo: parsing/ast.cmi parsing/astterm.cmi \
+    pretyping/classops.cmi toplevel/command.cmi parsing/coqast.cmi \
+    library/declare.cmi kernel/environ.cmi kernel/evd.cmi parsing/extend.cmi \
+    library/global.cmi library/goptions.cmi library/impargs.cmi \
+    library/lib.cmi library/libobject.cmi library/library.cmi \
+    proofs/macros.cmi toplevel/metasyntax.cmi kernel/names.cmi \
+    library/nametab.cmi lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi \
+    lib/pp.cmi lib/pp_control.cmi parsing/pretty.cmi parsing/printer.cmi \
     proofs/proof_trees.cmi kernel/reduction.cmi proofs/refiner.cmi \
-    lib/stamps.cmi library/states.cmi lib/system.cmi proofs/tacmach.cmi \
-    kernel/term.cmi pretyping/typing.cmi toplevel/vernacinterp.cmi \
-    toplevel/vernacentries.cmi 
-toplevel/vernacentries.cmx: parsing/ast.cmx pretyping/class.cmi \
-    pretyping/classops.cmx parsing/coqast.cmx library/declare.cmx \
-    kernel/environ.cmx kernel/evd.cmx parsing/extend.cmi library/global.cmx \
-    library/libobject.cmx library/library.cmx proofs/macros.cmx \
-    kernel/names.cmx library/nametab.cmx lib/options.cmx parsing/pcoq.cmi \
-    proofs/pfedit.cmx lib/pp.cmx lib/pp_control.cmx parsing/pretty.cmx \
+    toplevel/searchisos.cmi lib/stamps.cmi library/states.cmi lib/system.cmi \
+    proofs/tacmach.cmi kernel/term.cmi kernel/typeops.cmi lib/util.cmi \
+    toplevel/vernacinterp.cmi toplevel/vernacentries.cmi 
+toplevel/vernacentries.cmx: parsing/ast.cmx parsing/astterm.cmx \
+    pretyping/classops.cmx toplevel/command.cmi parsing/coqast.cmx \
+    library/declare.cmx kernel/environ.cmx kernel/evd.cmx parsing/extend.cmi \
+    library/global.cmx library/goptions.cmx library/impargs.cmx \
+    library/lib.cmx library/libobject.cmx library/library.cmx \
+    proofs/macros.cmx toplevel/metasyntax.cmx kernel/names.cmx \
+    library/nametab.cmx lib/options.cmx parsing/pcoq.cmi proofs/pfedit.cmx \
+    lib/pp.cmx lib/pp_control.cmx parsing/pretty.cmx parsing/printer.cmx \
     proofs/proof_trees.cmx kernel/reduction.cmx proofs/refiner.cmx \
-    lib/stamps.cmx library/states.cmx lib/system.cmx proofs/tacmach.cmx \
-    kernel/term.cmx pretyping/typing.cmx toplevel/vernacinterp.cmx \
-    toplevel/vernacentries.cmi 
+    toplevel/searchisos.cmi lib/stamps.cmx library/states.cmx lib/system.cmx \
+    proofs/tacmach.cmx kernel/term.cmx kernel/typeops.cmx lib/util.cmx \
+    toplevel/vernacinterp.cmx toplevel/vernacentries.cmi 
 toplevel/vernacinterp.cmo: parsing/ast.cmi parsing/coqast.cmi lib/dyn.cmi \
     toplevel/himsg.cmi kernel/names.cmi lib/options.cmi lib/pp.cmi \
     proofs/proof_trees.cmi proofs/tacinterp.cmi lib/util.cmi \
diff --git a/Makefile b/Makefile
index 99d19a0aa6..c46f30851d 100644
--- a/Makefile
+++ b/Makefile
@@ -57,7 +57,8 @@ PRETYPING=pretyping/typing.cmo pretyping/classops.cmo pretyping/recordops.cmo \
 PARSING=parsing/lexer.cmo parsing/coqast.cmo parsing/pcoq.cmo parsing/ast.cmo \
 	parsing/g_prim.cmo parsing/g_basevernac.cmo parsing/g_vernac.cmo \
 	parsing/g_command.cmo parsing/g_tactic.cmo parsing/g_multiple_case.cmo\
-        parsing/printer.cmo parsing/pretty.cmo parsing/astterm.cmo
+        parsing/printer.cmo parsing/pretty.cmo parsing/astterm.cmo \
+        parsing/egrammar.cmo
 
 PROOFS=proofs/tacred.cmo \
        proofs/proof_trees.cmo proofs/logic.cmo \
@@ -71,6 +72,7 @@ TACTICS=tactics/dn.cmo tactics/termdn.cmo tactics/btermdn.cmo \
         tactics/tacentries.cmo tactics/hiddentac.cmo tactics/elim.cmo
 
 TOPLEVEL=toplevel/himsg.cmo toplevel/errors.cmo toplevel/vernacinterp.cmo \
+         toplevel/metasyntax.cmo \
          toplevel/vernacentries.cmo toplevel/vernac.cmo toplevel/mltop.cmo \
 	 toplevel/protectedtoplevel.cmo toplevel/toplevel.cmo
 
@@ -91,6 +93,7 @@ link: $(LINK)
 	ocamlc -custom $(INCLUDES) -o link $(CMA) $(LINK) $(OSDEPLIBS)
 	rm -f link 
 
+lib: $(LIB)
 kernel: $(KERNEL)
 library: $(LIBRARY)
 proofs: $(PROOFS)
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 0d2d5cba50..0824c192cf 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -937,3 +937,27 @@ let type_fixpoint env sigma lna lar vdefj =
       (Array.map (fun j -> j.uj_type) vdefj) (Array.map body_of_type lar)
   with IllBranch i ->
     error_ill_typed_rec_body CCI env i lna vdefj lar
+
+
+(* A function which checks that a term well typed verifies both
+   syntaxic conditions *)
+
+let control_only_guard env sigma = 
+  let rec control_rec = function
+    | Rel(p)        -> ()
+    | VAR _         -> ()
+    | DOP0(_)       -> ()
+    | DOPN(CoFix(_),cl) as cofix ->
+	check_cofix env sigma cofix; 
+	Array.iter control_rec cl
+    | DOPN(Fix(_),cl) as fix  -> 
+	check_fix env sigma fix; 
+        Array.iter control_rec cl
+    | DOPN(_,cl)    -> Array.iter control_rec cl
+    | DOPL(_,cl)    -> List.iter control_rec cl
+    | DOP1(_,c)     -> control_rec c
+    | DOP2(_,c1,c2) -> control_rec c1; control_rec c2
+    | DLAM(_,c)     -> control_rec c
+    | DLAMV(_,v)    -> Array.iter control_rec v
+  in 
+  control_rec 
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 4f47bfd886..b935efd8c6 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -64,6 +64,7 @@ val apply_rel_list :
 
 val check_fix : env -> 'a evar_map -> constr -> unit
 val check_cofix : env -> 'a evar_map -> constr -> unit
+val control_only_guard : env -> 'a evar_map -> constr -> unit
 
 val type_fixpoint : env -> 'a evar_map -> name list -> typed_type array 
     -> unsafe_judgment array -> constraints
diff --git a/lib/options.ml b/lib/options.ml
index c4afa1e390..c0f14ee30b 100644
--- a/lib/options.ml
+++ b/lib/options.ml
@@ -1,6 +1,8 @@
 
 (* $Id$ *)
 
+open Util
+
 let batch_mode = ref false
 
 let debug = ref false
@@ -41,3 +43,10 @@ let without_mes_ambig f x =
   try make_mes_ambig false;
       let rslt = f x in (make_mes_ambig old; rslt)
   with e -> (make_mes_ambig old; raise e)
+
+(* A list of the areas of the system where "unsafe" operation
+ * has been requested *)
+let unsafe_set = ref Stringset.empty
+let add_unsafe s = unsafe_set := Stringset.add s !unsafe_set
+let is_unsafe s = Stringset.mem s !unsafe_set
+
diff --git a/lib/options.mli b/lib/options.mli
index 528226360e..9137883523 100644
--- a/lib/options.mli
+++ b/lib/options.mli
@@ -22,3 +22,6 @@ val make_mes_ambig : bool -> unit
 val is_mes_ambig : unit -> bool
 val without_mes_ambig : ('a -> 'b) -> 'a -> 'b
 
+val add_unsafe : string -> unit
+val is_unsafe : string -> bool
+
diff --git a/lib/system.ml b/lib/system.ml
index 0f005bd47f..9da302d302 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -3,6 +3,7 @@
 
 open Pp
 open Util
+open Unix
 
 (* Files and load path. *)
 
@@ -14,6 +15,37 @@ let del_path dir =
   if List.mem dir !load_path then
     load_path := List.filter (fun s -> s <> dir) !load_path
 
+let search_paths () = !load_path
+
+(* All subdirectories, recursively *)
+
+let all_subdirs dir =
+  let l = ref [] in
+  let add f = l := f :: !l in
+  let rec traverse dir =
+    Printf.printf "%s\n" dir;
+    let dirh = 
+      try opendir dir with Unix_error _ -> invalid_arg "all_subdirs" 
+    in
+    try
+      while true do
+	let f = readdir dirh in
+	if f <> "." && f <> ".." then
+	  let file = Filename.concat dir f in
+	  if (stat file).st_kind = S_DIR then begin
+	    add file;
+	    traverse file
+	  end
+      done
+    with End_of_file ->
+      closedir dirh
+  in
+  traverse dir; List.rev !l
+
+let radd_path dir = List.iter add_path (all_subdirs dir)
+
+
+
 (* TODO: rétablir glob (expansion ~user et $VAR) si on le juge nécessaire *)
 let glob s = s
 
@@ -50,26 +82,6 @@ let is_in_path lpath filename =
 let make_suffix name suffix =
   if Filename.check_suffix name suffix then name else (name ^ suffix)
 
-(*Gives the list of all the directories under dir*)
-let alldir dir =
-  let ini = Unix.getcwd()
-  and tmp = Filename.temp_file "coq" "rec"
-  and lst = ref [] in
-  Unix.chdir dir;
-  let bse = Unix.getcwd() in
-  let _ = Sys.command ("find "^bse^" -type d >> "^tmp) in
-  let inf = open_in tmp in
-  try
-    while true do
-      lst := !lst @ [input_line inf]
-    done;
-    []
-  with End_of_file ->
-    close_in inf;
-    Sys.remove tmp;
-    Unix.chdir ini;
-    !lst
-
 let open_trapping_failure open_fun name suffix =
   let rname = make_suffix name suffix in
   try open_fun rname with _ -> error ("Can't open " ^ rname)
diff --git a/lib/system.mli b/lib/system.mli
index 6f89901aa5..0c4bbd2284 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -3,7 +3,7 @@
 
 (*s Files. *)
 
-val alldir : string -> string list
+val all_subdirs : string -> string list
 val is_in_path : string list -> string -> bool
 val where_in_path : string list -> string -> string
 
@@ -15,6 +15,9 @@ val glob : string -> string
 
 val add_path : string -> unit
 val del_path : string -> unit
+val radd_path : string -> unit
+
+val search_paths : unit -> string list
 
 val find_file_in_path : string -> string
 
diff --git a/lib/util.ml b/lib/util.ml
index 59f119a50c..0cab4540e2 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -207,6 +207,12 @@ let list_map_append f l = List.flatten (List.map f l)
 
 let list_map_append2 f l1 l2 = List.flatten (List.map2 f l1 l2)
 
+let list_share_tails l1 l2 =
+  let rec shr_rev acc = function
+    | ((x1::l1), (x2::l2)) when x1 == x2 -> shr_rev (x1::acc) (l1,l2)
+    | (l1,l2) -> (List.rev l1, List.rev l2, acc)
+  in 
+  shr_rev [] (List.rev l1, List.rev l2)
 
 (* Arrays *)
 
diff --git a/lib/util.mli b/lib/util.mli
index b8b72da090..a3a20aaacf 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -62,6 +62,7 @@ val list_prefix_of : 'a list -> 'a list -> bool
 val list_map_append : ('a -> 'b list) -> 'a list -> 'b list
 (* raises [Invalid_argument] if the two lists don't have the same length *)
 val list_map_append2 : ('a -> 'b -> 'c list) -> 'a list -> 'b list -> 'c list
+val list_share_tails : 'a list -> 'a list -> 'a list * 'a list * 'a list
 
 (*s Arrays. *)
 
diff --git a/library/declare.ml b/library/declare.ml
index 067274aa73..7dca2b1c8a 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -22,18 +22,29 @@ let make_strength = function
   | [] -> NeverDischarge
   | l  -> DischargeAt (sp_of_wd l)
 
+let make_strength_0 () = make_strength (Lib.cwd())
+
+let make_strength_1 () =
+  let path = try List.tl (List.tl (Lib.cwd())) with Failure _ -> [] in
+  make_strength path
+
+let make_strength_2 () =
+  let path = try List.tl (Lib.cwd()) with Failure _ -> [] in
+  make_strength path
+
+
 (* Variables. *)
 
-type variable_declaration = identifier * constr * strength * bool
+type variable_declaration = constr * strength * bool
 
-let vartab = ref (Spmap.empty : variable_declaration Spmap.t)
+let vartab = ref (Spmap.empty : (identifier * variable_declaration) Spmap.t)
 
 let _ = Summary.declare_summary "VARIABLE"
 	  { Summary.freeze_function = (fun () -> !vartab);
 	    Summary.unfreeze_function = (fun ft -> vartab := ft);
 	    Summary.init_function = (fun () -> vartab := Spmap.empty) }
 
-let cache_variable (sp,((id,ty,_,_) as vd)) = 
+let cache_variable (sp,(id,(ty,_,_) as vd)) = 
   Global.push_var (id,ty);
   Nametab.push id sp;
   vartab := Spmap.add sp vd !vartab
@@ -55,9 +66,9 @@ let (in_variable, out_variable) =
     specification_function = specification_variable } in
   declare_object ("VARIABLE", od)
 
-let declare_variable ((id,ty,_,_) as obj) =
+let declare_variable id ((ty,_,_) as obj) =
   Global.push_var (id,ty);
-  let sp = add_leaf id CCI (in_variable obj) in
+  let sp = add_leaf id CCI (in_variable (id,obj)) in
   Nametab.push id sp
 
 (* Parameters. *)
@@ -86,7 +97,7 @@ let declare_parameter id c =
  
 (* Constants. *)
 
-type constant_declaration = identifier * constant_entry * strength * bool
+type constant_declaration = constant_entry * strength * bool
 
 let csttab = ref (Spmap.empty : constant_declaration Spmap.t)
 
@@ -114,7 +125,7 @@ let (in_constant, out_constant) =
     specification_function = specification_constant } in
   declare_object ("CONSTANT", od)
 
-let declare_constant ((id,ce,_,_) as cd) =
+let declare_constant id ((ce,_,_) as cd) =
   let sp = add_leaf id CCI (in_constant ce) in
   Global.add_constant sp ce;
   Nametab.push (basename sp) sp;
@@ -204,13 +215,13 @@ let is_variable id =
   let sp = Nametab.sp_of_id CCI id in Spmap.mem sp !vartab
   
 let out_variable sp = 
-  let (id,_,str,sticky) = Spmap.find sp !vartab in
+  let (id,(_,str,sticky)) = Spmap.find sp !vartab in
   let (_,ty) = Global.lookup_var id in
   (id,ty,str,sticky)
 
 let variable_strength id =
   let sp = Nametab.sp_of_id CCI id in 
-  let (_,_,str,_) = Spmap.find sp !vartab in
+  let _,(_,str,_) = Spmap.find sp !vartab in
   str
 
 (* Global references. *)
@@ -293,8 +304,8 @@ let declare_eliminations sp =
   let redmind = minductype_spec env sigma mind in
   let mindstr = string_of_id mindid in
   let declare na c =
-    declare_constant 
-      (id_of_string na, { const_entry_body = c; const_entry_type = None },
+    declare_constant (id_of_string na)
+      ({ const_entry_body = c; const_entry_type = None },
        false, NeverDischarge)
   in
   let mispec = Global.lookup_mind_specif redmind in 
diff --git a/library/declare.mli b/library/declare.mli
index 952fa0500b..1a9a0fac21 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -20,14 +20,14 @@ type strength =
   | DischargeAt of section_path 
   | NeverDischarge
 
-type variable_declaration = identifier * constr * strength * bool
+type variable_declaration = constr * strength * bool
 
-val declare_variable : variable_declaration -> unit
+val declare_variable : identifier -> variable_declaration -> unit
 
 
-type constant_declaration = identifier * constant_entry * strength * bool
+type constant_declaration = constant_entry * strength * bool
 
-val declare_constant : constant_declaration -> unit
+val declare_constant : identifier -> constant_declaration -> unit
 
 val declare_parameter : identifier -> constr -> unit
 
@@ -41,6 +41,9 @@ val declare_eliminations : section_path -> unit
 val declare_syntax_constant : identifier -> constr -> unit
 
 val make_strength : string list -> strength
+val make_strength_0 : unit -> strength
+val make_strength_1 : unit -> strength
+val make_strength_2 : unit -> strength
 
 (*s Corresponding test and access functions. *)
 
diff --git a/library/impargs.ml b/library/impargs.ml
index 2cc34c3cb4..cd9a5ef4e1 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -15,6 +15,21 @@ type implicits =
 
 let implicit_args = ref false
 
+let make_implicit_args flag = implicit_args := flag
+let is_implicit_args () = !implicit_args
+
+let implicitely f x =
+  let oimplicit = !implicit_args in
+  try 
+    implicit_args := true;
+    let rslt = f x in 
+    implicit_args := oimplicit;
+    rslt
+  with e -> begin
+    implicit_args := oimplicit;
+    raise e
+  end
+
 let auto_implicits ty =
   if !implicit_args then
     let genv = Global.env() in
diff --git a/library/impargs.mli b/library/impargs.mli
index 51ada5845a..8a598ef7e8 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -14,7 +14,9 @@ type implicits =
   | Impl_manual of int list
   | No_impl
 
-val implicit_args : bool ref
+val make_implicit_args : bool -> unit
+val is_implicit_args : unit -> bool
+val implicitely : ('a -> 'b) -> 'a -> 'b
 
 val list_of_implicits : implicits -> int list
 
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 18a9b09a74..a9a8e0d3b6 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -8,14 +8,17 @@ open Sign
 open Generic
 open Term
 open Constant
+open Environ
 open Evd
 open Declare
+open Typing
 open Tacmach
 open Proof_trees
 open Lib
+open Astterm
 
 type proof_topstate = {
-  top_hyps : var_context * var_context;
+  top_hyps : env * env;
   top_goal : goal;
   top_strength : strength }
 
@@ -61,8 +64,8 @@ let get_evmap_sign og =
 	  None 
   in
   match og with
-    | Some goal -> (project goal, pf_hyps goal)
-    | _ -> (Evd.empty, Global.var_context())
+    | Some goal -> (project goal, pf_env goal)
+    | _ -> (Evd.empty, Global.env())
  
 let set_proof s = 
   try 
@@ -171,8 +174,9 @@ let save_named opacity =
   let {evar_concl=concl} = ts.top_goal 
   and strength = ts.top_strength in
   let pfterm = extract_pftreestate pfs in 
-  declare_constant (id_of_string ident) (*** opacity strength ***) 
-    { const_entry_body = pfterm; const_entry_type = Some concl };
+  declare_constant (id_of_string ident)
+    ({ const_entry_body = pfterm; const_entry_type = Some concl },
+      strength, opacity);
   del_proof ident;
   message(ident ^ " is defined")
     
@@ -183,12 +187,14 @@ let save_anonymous opacity save_ident n =
   and strength = ts.top_strength in
   let pfterm = extract_pftreestate pfs in 
   if ident = "Unnamed_thm" then
-    declare_constant (id_of_string save_ident) (*** opacity,strength ***)
-      { const_entry_body = pfterm; const_entry_type = Some concl }
+    declare_constant (id_of_string save_ident)
+      ({ const_entry_body = pfterm; const_entry_type = Some concl },
+       strength, opacity)
   else begin
     message("Overriding name " ^ ident ^ " and using " ^ save_ident);
-    declare_constant (id_of_string save_ident) (*** opacity,strength ***)
-      { const_entry_body = pfterm; const_entry_type = Some concl }
+    declare_constant (id_of_string save_ident)
+      ({ const_entry_body = pfterm; const_entry_type = Some concl },
+       strength, opacity)
   end;
   del_proof ident;
   message(save_ident ^ " is defined")
@@ -241,10 +247,10 @@ and reset_initial () = restore_state "Initial"
 (*              Modifying the current prooftree                      *)
 (*********************************************************************)
 
-let start_proof_with_type na str sign fsign concl =
-  let top_goal = mk_goal (mt_ctxt Intset.empty) sign concl in
+let start_proof_with_type na str env concl =
+  let top_goal = mk_goal (mt_ctxt Intset.empty) env concl in
   let ts = { 
-    top_hyps = (sign,fsign);
+    top_hyps = (env,empty_env);
     top_goal = top_goal;
     top_strength = str }
   in
@@ -252,14 +258,16 @@ let start_proof_with_type na str sign fsign concl =
   set_proof (Some na)
 
 let start_proof na str concl_com =
-  let (sigma,(sign,fsign)) = initial_sigma_assumptions() in
-  let concl = fconstruct_type sigma sign concl_com in
-  start_proof_with_type na str sign fsign concl.body
+  let sigma = Evd.empty in
+  let env = Global.env() in
+  let concl = fconstruct_type sigma (Environ.context env) concl_com in
+  start_proof_with_type na str env concl.body
 
 let start_proof_constr na str concl =
-  let (sigma,(sign,fsign)) = initial_sigma_assumptions() in
-  let _ = type_of_type sigma sign concl in
-  start_proof_with_type na str sign fsign concl
+  let sigma = Evd.empty in
+  let env = Global.env() in
+  let _ = execute_type env sigma concl in
+  start_proof_with_type na str env concl
 
 let solve_nth k tac =
   let pft = get_pftreestate() in
@@ -301,7 +309,7 @@ let traverse n = rev_mutate (traverse n)
 
 let rec nth_cdr = function
   | 0 -> (function l -> l)
-  | n -> (comp List.tl (nth_cdr (n - 1)))
+  | n -> (compose List.tl (nth_cdr (n - 1)))
 	
 let rec common_ancestor_equal_length = function
   | ((a::l1), (b::l2)) ->
@@ -319,7 +327,7 @@ let rec common_ancestor_equal_length = function
 let common_ancestor l1 l2 =
   let diff_lengths = (List.length l1) - (List.length l2) in
   if diff_lengths > 0 then
-    let head,tail = chop_list diff_lengths l1 in
+    let head,tail = list_chop diff_lengths l1 in
     let (prefx,n) = common_ancestor_equal_length (tail,l2) in 
     (head@prefx),n
   else if diff_lengths < 0 then
@@ -347,3 +355,11 @@ let traverse_to path =
 
 (* traverse the proof tree until it reach the nth subgoal *)
 let traverse_nth_goal n = mutate (nth_unproven n)
+
+(* The goal focused on *)
+let focus_n = ref 0
+let make_focus n = focus_n := n
+let focus () = !focus_n
+let focused_goal () = let n = !focus_n in if n=0 then 1 else n
+
+
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 7a953dff6e..3e86b38624 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -3,7 +3,9 @@
 
 (*i*)
 open Pp
+open Term
 open Sign
+open Environ
 open Declare
 open Proof_trees
 open Tacmach
@@ -11,21 +13,27 @@ open Tacmach
 
 val proof_prompt : unit -> string
 val refining : unit -> bool
+val abort_goal : string -> unit
+val abort_cur_goal : unit -> unit
+val abort_goals : unit -> unit
+val abort_refine : ('a -> 'b) -> 'a -> 'b
 val msg_proofs : bool -> std_ppcmds
 
 val undo_limit : int ref
 val set_undo : int -> unit
 val unset_undo : unit -> unit
+val undo : int -> unit
+val resume_last : unit -> unit
 
 type proof_topstate = {
-  top_hyps : context * context;
+  top_hyps : env * env;
   top_goal : goal;
   top_strength : strength }
 
 val get_state : unit -> pftreestate * proof_topstate
 val get_topstate : unit -> proof_topstate
 val get_pftreestate : unit -> pftreestate
-val get_evmap_sign : int option -> evar_declarations * context
+val get_evmap_sign : int option -> evar_declarations * env
 val set_proof : string option -> unit
 val get_proof : unit -> string
 val list_proofs : unit -> string list
@@ -33,6 +41,27 @@ val add_proof : string * pftreestate * proof_topstate -> unit
 val del_proof : string -> unit
 val init_proofs : unit -> unit
 
+val mutate : (pftreestate -> pftreestate) -> unit
+val rev_mutate : (pftreestate -> pftreestate) -> unit
+val start : string * proof_topstate -> unit
+val restart : unit -> unit
+val proof_prompt : unit -> string
+val proof_term : unit -> constr
+
+val start_proof : string -> strength -> Coqast.t -> unit
+val start_proof_constr : string -> strength -> constr -> unit
+
+val save_named : bool -> unit
+val save_anonymous : bool -> string -> 'a -> unit
+val save_anonymous_thm : bool -> string -> unit
+val save_anonymous_remark : bool -> string -> unit
+
+val solve_nth : int -> tactic -> unit
+val by : tactic -> unit
+val traverse : int -> unit
+val traverse_nth_goal : int -> unit
+val traverse_to : int list -> unit
+
 val make_focus : int -> unit
 val focus : unit -> int
 val focused_goal : unit -> int
diff --git a/tactics/pattern.ml b/tactics/pattern.ml
index 297b26bb8e..52b6586b5c 100644
--- a/tactics/pattern.ml
+++ b/tactics/pattern.ml
@@ -31,7 +31,7 @@ let rec whd_replmeta = function
 let raw_sopattern_of_compattern sign com =
   failwith "raw_sopattern_of_compattern: TODO"
   (***
-  let c = Astterm.raw_constr_of_compattern empty_evd (gLOB sign) com in
+  let c = Astterm.raw_constr_of_compattern Evd.empty (gLOB sign) com in
   strong whd_replmeta c
   ***)