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

4 files changed, 99 insertions, 64 deletions

diff --git a/.depend b/.depend
index 428c901f36..c0e322ea75 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 
diff --git a/CHANGES b/CHANGES
index 6ebd9b2811..61445214cd 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,12 +1,21 @@
 Changes from V7.4
 =================
 
+A revision of the standard library and of concrete syntax of Coq, including
+
+- a completely new syntax for terms
+- renaming of various standard notions from French to English (esp in ZArith)
+- all notions of the standard library are declared with (strict)
+  implicit arguments
+
 Vernacular commands
 
 - "Declare ML Module" now allows us to import .cma files. This avoids to use a
    bunch of "Declare ML Module" statements when using several ML files.
 - "Set Printing Width n" added, allows to change the size of width printing
    (TODO : doc).
+- "Implicit Variables Type x,y:t" assigns default types for binding variables.
+
 Gallina
 
 - New syntax of the form "Inductive bool : Set := true, false : bool." for
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index b314a73aeb..cd0d99581e 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -27,6 +27,7 @@ open Rawterm
 open Pattern
 open Nametab
 open Symbols
+open Reserve
 (*i*)
 
 (* Translation from rawconstr to front constr *)
@@ -239,12 +240,12 @@ let rec extern scopes vars r =
               extern scopes (add_vname vars na) c)
 
   | RProd (loc,na,t,c) ->
-      let t = extern scopes vars t in
+      let t = extern scopes vars (anonymize_if_reserved na t) in
       let (idl,c) = factorize_prod scopes (add_vname vars na) t c in
       CProdN (loc,[(dummy_loc,na)::idl,t],c)
 
   | RLambda (loc,na,t,c) ->
-      let t = extern scopes vars t in
+      let t = extern scopes vars (anonymize_if_reserved na t) in
       let (idl,c) = factorize_lambda scopes (add_vname vars na) t c in
       CLambdaN (loc,[(dummy_loc,na)::idl,t],c)
 
@@ -292,8 +293,8 @@ let rec extern scopes vars r =
   | RDynamic (loc,d) -> CDynamic (loc,d)
 	
 and factorize_prod scopes vars aty = function
-  | RProd (loc,Name id,ty,c)
-      when aty = extern scopes vars ty
+  | RProd (loc,(Name id as na),ty,c)
+      when aty = extern scopes vars (anonymize_if_reserved na ty)
 	& not (occur_var_constr_expr id aty) (* avoid na in ty escapes scope *)
 	-> let (nal,c) = factorize_prod scopes (Idset.add id vars) aty c in
            ((loc,Name id)::nal,c)
@@ -301,7 +302,7 @@ and factorize_prod scopes vars aty = function
 
 and factorize_lambda scopes vars aty = function
   | RLambda (loc,na,ty,c)
-      when aty = extern scopes vars ty
+      when aty = extern scopes vars (anonymize_if_reserved na ty)
 	& not (occur_name na aty) (* To avoid na in ty' escapes scope *)
 	-> let (nal,c) = factorize_lambda scopes (add_vname vars na) aty c in
            ((loc,na)::nal,c)
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index 2d86e00c93..eee2042a00 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -456,7 +456,19 @@ let pr_lconstr_env env c = pr ltop (transf env c)
 let pr_constr c = pr_constr_env (Global.env()) c
 let pr_lconstr c = pr_lconstr_env (Global.env()) c
 
-let pr_binders = pr_binders pr
+let anonymize_binder na c =
+  if Options.do_translate() then
+    Constrextern.extern_rawconstr (Termops.vars_of_env (Global.env()))
+      (Reserve.anonymize_if_reserved na
+      (Constrintern.for_grammar
+        (Constrintern.interp_rawconstr Evd.empty (Global.env())) c))
+  else c
+
+let pr_binders l =
+  prlist_with_sep sep
+    (fun (nal,t) -> prlist_with_sep sep
+      (fun (_,na as x) -> pr_oneb pr (anonymize_binder na t) x) nal) l
+
 let pr_cases_pattern = pr_patt ltop
 
 let pr_pattern = pr_constr