Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)

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

1 files changed, 71 insertions, 58 deletions

diff --git a/.depend b/.depend
index 428c901f3..c0e322ea7 100644
--- a/.depend
+++ b/.depend
@@ -15,6 +15,7 @@ interp/genarg.cmi: pretyping/evd.cmi library/libnames.cmi kernel/names.cmi \
 interp/modintern.cmi: kernel/declarations.cmi kernel/entries.cmi \
     kernel/environ.cmi interp/topconstr.cmi 
 interp/ppextend.cmi: kernel/names.cmi lib/pp.cmi 
+interp/reserve.cmi: kernel/names.cmi pretyping/rawterm.cmi 
 interp/symbols.cmi: lib/bignat.cmi library/libnames.cmi kernel/names.cmi \
     library/nametab.cmi lib/pp.cmi interp/ppextend.cmi pretyping/rawterm.cmi \
     interp/topconstr.cmi lib/util.cmi 
@@ -495,34 +496,34 @@ interp/constrextern.cmo: pretyping/classops.cmi library/declare.cmi \
     pretyping/detyping.cmi kernel/environ.cmi library/impargs.cmi \
     kernel/inductive.cmi library/libnames.cmi library/nameops.cmi \
     kernel/names.cmi library/nametab.cmi pretyping/pattern.cmi lib/pp.cmi \
-    pretyping/rawterm.cmi kernel/sign.cmi interp/symbols.cmi kernel/term.cmi \
-    pretyping/termops.cmi interp/topconstr.cmi kernel/univ.cmi lib/util.cmi \
-    interp/constrextern.cmi 
+    pretyping/rawterm.cmi interp/reserve.cmi kernel/sign.cmi \
+    interp/symbols.cmi kernel/term.cmi pretyping/termops.cmi \
+    interp/topconstr.cmi kernel/univ.cmi lib/util.cmi interp/constrextern.cmi 
 interp/constrextern.cmx: pretyping/classops.cmx library/declare.cmx \
     pretyping/detyping.cmx kernel/environ.cmx library/impargs.cmx \
     kernel/inductive.cmx library/libnames.cmx library/nameops.cmx \
     kernel/names.cmx library/nametab.cmx pretyping/pattern.cmx lib/pp.cmx \
-    pretyping/rawterm.cmx kernel/sign.cmx interp/symbols.cmx kernel/term.cmx \
-    pretyping/termops.cmx interp/topconstr.cmx kernel/univ.cmx lib/util.cmx \
-    interp/constrextern.cmi 
+    pretyping/rawterm.cmx interp/reserve.cmx kernel/sign.cmx \
+    interp/symbols.cmx kernel/term.cmx pretyping/termops.cmx \
+    interp/topconstr.cmx kernel/univ.cmx lib/util.cmx interp/constrextern.cmi 
 interp/constrintern.cmo: lib/bignat.cmi library/declare.cmi \
     kernel/environ.cmi pretyping/evd.cmi library/global.cmi \
     library/impargs.cmi library/libnames.cmi library/nameops.cmi \
     kernel/names.cmi library/nametab.cmi lib/options.cmi \
     pretyping/pattern.cmi lib/pp.cmi pretyping/pretype_errors.cmi \
-    pretyping/pretyping.cmi pretyping/rawterm.cmi pretyping/retyping.cmi \
-    kernel/sign.cmi interp/symbols.cmi interp/syntax_def.cmi kernel/term.cmi \
-    pretyping/termops.cmi interp/topconstr.cmi lib/util.cmi \
-    interp/constrintern.cmi 
+    pretyping/pretyping.cmi pretyping/rawterm.cmi interp/reserve.cmi \
+    pretyping/retyping.cmi kernel/sign.cmi interp/symbols.cmi \
+    interp/syntax_def.cmi kernel/term.cmi pretyping/termops.cmi \
+    interp/topconstr.cmi lib/util.cmi interp/constrintern.cmi 
 interp/constrintern.cmx: lib/bignat.cmx library/declare.cmx \
     kernel/environ.cmx pretyping/evd.cmx library/global.cmx \
     library/impargs.cmx library/libnames.cmx library/nameops.cmx \
     kernel/names.cmx library/nametab.cmx lib/options.cmx \
     pretyping/pattern.cmx lib/pp.cmx pretyping/pretype_errors.cmx \
-    pretyping/pretyping.cmx pretyping/rawterm.cmx pretyping/retyping.cmx \
-    kernel/sign.cmx interp/symbols.cmx interp/syntax_def.cmx kernel/term.cmx \
-    pretyping/termops.cmx interp/topconstr.cmx lib/util.cmx \
-    interp/constrintern.cmi 
+    pretyping/pretyping.cmx pretyping/rawterm.cmx interp/reserve.cmx \
+    pretyping/retyping.cmx kernel/sign.cmx interp/symbols.cmx \
+    interp/syntax_def.cmx kernel/term.cmx pretyping/termops.cmx \
+    interp/topconstr.cmx lib/util.cmx interp/constrintern.cmi 
 interp/coqlib.cmo: library/declare.cmi library/libnames.cmi kernel/names.cmi \
     library/nametab.cmi pretyping/pattern.cmi kernel/term.cmi lib/util.cmi \
     interp/coqlib.cmi 
@@ -547,6 +548,12 @@ interp/ppextend.cmo: kernel/names.cmi lib/pp.cmi lib/util.cmi \
     interp/ppextend.cmi 
 interp/ppextend.cmx: kernel/names.cmx lib/pp.cmx lib/util.cmx \
     interp/ppextend.cmi 
+interp/reserve.cmo: library/lib.cmi library/libobject.cmi library/nameops.cmi \
+    kernel/names.cmi pretyping/rawterm.cmi library/summary.cmi lib/util.cmi \
+    interp/reserve.cmi 
+interp/reserve.cmx: library/lib.cmx library/libobject.cmx library/nameops.cmx \
+    kernel/names.cmx pretyping/rawterm.cmx library/summary.cmx lib/util.cmx \
+    interp/reserve.cmi 
 interp/symbols.cmo: lib/bignat.cmi lib/gmapl.cmi library/lib.cmi \
     library/libnames.cmi library/libobject.cmi library/library.cmi \
     kernel/names.cmi library/nametab.cmi lib/options.cmi lib/pp.cmi \
@@ -2150,43 +2157,45 @@ toplevel/vernac.cmx: parsing/coqast.cmx parsing/lexer.cmx library/lib.cmx \
 toplevel/vernacentries.cmo: tactics/auto.cmi toplevel/class.cmi \
     pretyping/classops.cmi toplevel/command.cmi interp/constrextern.cmi \
     interp/constrintern.cmi library/decl_kinds.cmo library/declaremods.cmi \
-    tactics/dhyp.cmi toplevel/discharge.cmi kernel/entries.cmi \
-    kernel/environ.cmi pretyping/evarutil.cmi pretyping/evd.cmi \
-    library/global.cmi library/goptions.cmi library/impargs.cmi \
-    pretyping/inductiveops.cmi library/lib.cmi library/libnames.cmi \
-    library/library.cmi toplevel/metasyntax.cmi toplevel/mltop.cmi \
-    interp/modintern.cmi library/nameops.cmi kernel/names.cmi \
-    library/nametab.cmi lib/options.cmi proofs/pfedit.cmi lib/pp.cmi \
-    lib/pp_control.cmi parsing/prettyp.cmi pretyping/pretyping.cmi \
+    pretyping/detyping.cmi tactics/dhyp.cmi toplevel/discharge.cmi \
+    kernel/entries.cmi kernel/environ.cmi pretyping/evarutil.cmi \
+    pretyping/evd.cmi library/global.cmi library/goptions.cmi \
+    library/impargs.cmi pretyping/inductiveops.cmi library/lib.cmi \
+    library/libnames.cmi library/library.cmi toplevel/metasyntax.cmi \
+    toplevel/mltop.cmi interp/modintern.cmi library/nameops.cmi \
+    kernel/names.cmi library/nametab.cmi lib/options.cmi proofs/pfedit.cmi \
+    lib/pp.cmi lib/pp_control.cmi parsing/prettyp.cmi pretyping/pretyping.cmi \
     parsing/printer.cmi parsing/printmod.cmi proofs/proof_trees.cmi \
     proofs/proof_type.cmi toplevel/record.cmi toplevel/recordobj.cmi \
-    pretyping/reductionops.cmi proofs/refiner.cmi kernel/safe_typing.cmi \
-    parsing/search.cmi library/states.cmi interp/symbols.cmi lib/system.cmi \
-    tactics/tacinterp.cmi proofs/tacmach.cmi pretyping/tacred.cmi \
-    proofs/tactic_debug.cmi tactics/tactics.cmi kernel/term.cmi \
-    parsing/termast.cmi interp/topconstr.cmi kernel/typeops.cmi \
-    kernel/univ.cmi lib/util.cmi toplevel/vernacexpr.cmo \
-    toplevel/vernacinterp.cmi toplevel/vernacentries.cmi 
+    pretyping/reductionops.cmi proofs/refiner.cmi interp/reserve.cmi \
+    kernel/safe_typing.cmi parsing/search.cmi library/states.cmi \
+    interp/symbols.cmi lib/system.cmi tactics/tacinterp.cmi \
+    proofs/tacmach.cmi pretyping/tacred.cmi proofs/tactic_debug.cmi \
+    tactics/tactics.cmi kernel/term.cmi parsing/termast.cmi \
+    interp/topconstr.cmi kernel/typeops.cmi kernel/univ.cmi lib/util.cmi \
+    toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi \
+    toplevel/vernacentries.cmi 
 toplevel/vernacentries.cmx: tactics/auto.cmx toplevel/class.cmx \
     pretyping/classops.cmx toplevel/command.cmx interp/constrextern.cmx \
     interp/constrintern.cmx library/decl_kinds.cmx library/declaremods.cmx \
-    tactics/dhyp.cmx toplevel/discharge.cmx kernel/entries.cmx \
-    kernel/environ.cmx pretyping/evarutil.cmx pretyping/evd.cmx \
-    library/global.cmx library/goptions.cmx library/impargs.cmx \
-    pretyping/inductiveops.cmx library/lib.cmx library/libnames.cmx \
-    library/library.cmx toplevel/metasyntax.cmx toplevel/mltop.cmx \
-    interp/modintern.cmx library/nameops.cmx kernel/names.cmx \
-    library/nametab.cmx lib/options.cmx proofs/pfedit.cmx lib/pp.cmx \
-    lib/pp_control.cmx parsing/prettyp.cmx pretyping/pretyping.cmx \
+    pretyping/detyping.cmx tactics/dhyp.cmx toplevel/discharge.cmx \
+    kernel/entries.cmx kernel/environ.cmx pretyping/evarutil.cmx \
+    pretyping/evd.cmx library/global.cmx library/goptions.cmx \
+    library/impargs.cmx pretyping/inductiveops.cmx library/lib.cmx \
+    library/libnames.cmx library/library.cmx toplevel/metasyntax.cmx \
+    toplevel/mltop.cmx interp/modintern.cmx library/nameops.cmx \
+    kernel/names.cmx library/nametab.cmx lib/options.cmx proofs/pfedit.cmx \
+    lib/pp.cmx lib/pp_control.cmx parsing/prettyp.cmx pretyping/pretyping.cmx \
     parsing/printer.cmx parsing/printmod.cmx proofs/proof_trees.cmx \
     proofs/proof_type.cmx toplevel/record.cmx toplevel/recordobj.cmx \
-    pretyping/reductionops.cmx proofs/refiner.cmx kernel/safe_typing.cmx \
-    parsing/search.cmx library/states.cmx interp/symbols.cmx lib/system.cmx \
-    tactics/tacinterp.cmx proofs/tacmach.cmx pretyping/tacred.cmx \
-    proofs/tactic_debug.cmx tactics/tactics.cmx kernel/term.cmx \
-    parsing/termast.cmx interp/topconstr.cmx kernel/typeops.cmx \
-    kernel/univ.cmx lib/util.cmx toplevel/vernacexpr.cmx \
-    toplevel/vernacinterp.cmx toplevel/vernacentries.cmi 
+    pretyping/reductionops.cmx proofs/refiner.cmx interp/reserve.cmx \
+    kernel/safe_typing.cmx parsing/search.cmx library/states.cmx \
+    interp/symbols.cmx lib/system.cmx tactics/tacinterp.cmx \
+    proofs/tacmach.cmx pretyping/tacred.cmx proofs/tactic_debug.cmx \
+    tactics/tactics.cmx kernel/term.cmx parsing/termast.cmx \
+    interp/topconstr.cmx kernel/typeops.cmx kernel/univ.cmx lib/util.cmx \
+    toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx \
+    toplevel/vernacentries.cmi 
 toplevel/vernacexpr.cmo: library/decl_kinds.cmo parsing/extend.cmi \
     interp/genarg.cmi library/goptions.cmi library/libnames.cmi \
     kernel/names.cmi library/nametab.cmi interp/ppextend.cmi \
@@ -2212,16 +2221,16 @@ translate/ppconstrnew.cmo: parsing/ast.cmi lib/bignat.cmi \
     pretyping/evd.cmi interp/genarg.cmi library/global.cmi \
     library/libnames.cmi library/nameops.cmi kernel/names.cmi \
     library/nametab.cmi lib/options.cmi lib/pp.cmi interp/ppextend.cmi \
-    pretyping/rawterm.cmi interp/symbols.cmi kernel/term.cmi \
-    pretyping/termops.cmi interp/topconstr.cmi lib/util.cmi \
+    pretyping/rawterm.cmi interp/reserve.cmi interp/symbols.cmi \
+    kernel/term.cmi pretyping/termops.cmi interp/topconstr.cmi lib/util.cmi \
     translate/ppconstrnew.cmi 
 translate/ppconstrnew.cmx: parsing/ast.cmx lib/bignat.cmx \
     interp/constrextern.cmx interp/constrintern.cmx parsing/coqast.cmx \
     pretyping/evd.cmx interp/genarg.cmx library/global.cmx \
     library/libnames.cmx library/nameops.cmx kernel/names.cmx \
     library/nametab.cmx lib/options.cmx lib/pp.cmx interp/ppextend.cmx \
-    pretyping/rawterm.cmx interp/symbols.cmx kernel/term.cmx \
-    pretyping/termops.cmx interp/topconstr.cmx lib/util.cmx \
+    pretyping/rawterm.cmx interp/reserve.cmx interp/symbols.cmx \
+    kernel/term.cmx pretyping/termops.cmx interp/topconstr.cmx lib/util.cmx \
     translate/ppconstrnew.cmi 
 translate/pptacticnew.cmo: kernel/closure.cmi lib/dyn.cmi kernel/environ.cmi \
     parsing/extend.cmi interp/genarg.cmi library/libnames.cmi \
@@ -2235,21 +2244,25 @@ translate/pptacticnew.cmx: kernel/closure.cmx lib/dyn.cmx kernel/environ.cmx \
     interp/ppextend.cmx parsing/pptactic.cmx pretyping/rawterm.cmx \
     proofs/tacexpr.cmx pretyping/termops.cmx interp/topconstr.cmx \
     lib/util.cmx translate/pptacticnew.cmi 
-translate/ppvernacnew.cmo: parsing/ast.cmi parsing/coqast.cmi \
-    library/decl_kinds.cmo parsing/egrammar.cmi parsing/extend.cmi \
+translate/ppvernacnew.cmo: parsing/ast.cmi interp/constrextern.cmi \
+    interp/constrintern.cmi parsing/coqast.cmi library/decl_kinds.cmo \
+    parsing/egrammar.cmi pretyping/evd.cmi parsing/extend.cmi \
     interp/genarg.cmi library/global.cmi library/goptions.cmi \
     library/libnames.cmi library/nameops.cmi kernel/names.cmi \
-    library/nametab.cmi parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.cmi \
-    translate/ppconstrnew.cmi interp/ppextend.cmi translate/pptacticnew.cmi \
-    pretyping/rawterm.cmi proofs/tacexpr.cmo interp/topconstr.cmi \
+    library/nametab.cmi lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi \
+    lib/pp.cmi translate/ppconstrnew.cmi interp/ppextend.cmi \
+    translate/pptacticnew.cmi pretyping/rawterm.cmi interp/reserve.cmi \
+    proofs/tacexpr.cmo pretyping/termops.cmi interp/topconstr.cmi \
     lib/util.cmi toplevel/vernacexpr.cmo translate/ppvernacnew.cmi 
-translate/ppvernacnew.cmx: parsing/ast.cmx parsing/coqast.cmx \
-    library/decl_kinds.cmx parsing/egrammar.cmx parsing/extend.cmx \
+translate/ppvernacnew.cmx: parsing/ast.cmx interp/constrextern.cmx \
+    interp/constrintern.cmx parsing/coqast.cmx library/decl_kinds.cmx \
+    parsing/egrammar.cmx pretyping/evd.cmx parsing/extend.cmx \
     interp/genarg.cmx library/global.cmx library/goptions.cmx \
     library/libnames.cmx library/nameops.cmx kernel/names.cmx \
-    library/nametab.cmx parsing/pcoq.cmx proofs/pfedit.cmx lib/pp.cmx \
-    translate/ppconstrnew.cmx interp/ppextend.cmx translate/pptacticnew.cmx \
-    pretyping/rawterm.cmx proofs/tacexpr.cmx interp/topconstr.cmx \
+    library/nametab.cmx lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx \
+    lib/pp.cmx translate/ppconstrnew.cmx interp/ppextend.cmx \
+    translate/pptacticnew.cmx pretyping/rawterm.cmx interp/reserve.cmx \
+    proofs/tacexpr.cmx pretyping/termops.cmx interp/topconstr.cmx \
     lib/util.cmx toplevel/vernacexpr.cmx translate/ppvernacnew.cmi 
 contrib/cc/ccalgo.cmo: kernel/names.cmi kernel/term.cmi contrib/cc/ccalgo.cmi 
 contrib/cc/ccalgo.cmx: kernel/names.cmx kernel/term.cmx contrib/cc/ccalgo.cmi