Subtac fixes, single fixpoint definitions are working again. Added a toggle on the pretyping

module to allow or disallow binding of syntaxically inexistant variables (i.e., under an if when applied to an inductive where
constructors have arguments). Does not change current behavior.


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

1 files changed, 33 insertions, 94 deletions

diff --git a/contrib/subtac/subtac_command.mli b/contrib/subtac/subtac_command.mli
index 23a03290c8..6c1b0103ff 100644
--- a/contrib/subtac/subtac_command.mli
+++ b/contrib/subtac/subtac_command.mli
@@ -1,103 +1,42 @@
-module SPretyping :
-  sig
-    module Cases :
-      sig
-        val compile_cases :
-          Util.loc ->
-          (Evarutil.type_constraint ->
-           Environ.env -> Rawterm.rawconstr -> Environ.unsafe_judgment) *
-          Evd.evar_defs ref ->
-          Evarutil.type_constraint ->
-          Environ.env ->
-          Rawterm.rawconstr option *
-          (Rawterm.rawconstr *
-           (Names.name *
-            (Util.loc * Names.inductive * Names.name list) option))
-          list *
-          (Util.loc * Names.identifier list * Rawterm.cases_pattern list *
-           Rawterm.rawconstr)
-          list -> Environ.unsafe_judgment
-      end
-    val understand_tcc :
-      Evd.evar_map ->
-      Environ.env ->
-      ?expected_type:Term.types -> Rawterm.rawconstr -> Evd.open_constr
-    val understand_ltac :
-      Evd.evar_map ->
-      Environ.env ->
-      Pretyping.var_map * Pretyping.unbound_ltac_var_map ->
-      Pretyping.typing_constraint ->
-      Rawterm.rawconstr -> Evd.evar_defs * Term.constr
-    val understand :
-      Evd.evar_map ->
-      Environ.env ->
-      ?expected_type:Term.types -> Rawterm.rawconstr -> Term.constr
-    val understand_type :
-      Evd.evar_map -> Environ.env -> Rawterm.rawconstr -> Term.constr
-    val understand_gen :
-      Pretyping.typing_constraint ->
-      Evd.evar_map -> Environ.env -> Rawterm.rawconstr -> Term.constr
-    val understand_judgment :
-      Evd.evar_map ->
-      Environ.env -> Rawterm.rawconstr -> Environ.unsafe_judgment
-    val understand_judgment_tcc :
-      Evd.evar_map ->
-      Environ.env ->
-      Rawterm.rawconstr -> Evd.evar_map * Environ.unsafe_judgment
-    val pretype :
-      Evarutil.type_constraint ->
-      Environ.env ->
-      Evd.evar_defs ref ->
-      Pretyping.var_map * (Names.identifier * Names.identifier option) list ->
-      Rawterm.rawconstr -> Environ.unsafe_judgment
-    val pretype_type :
-      Evarutil.val_constraint ->
-      Environ.env ->
-      Evd.evar_defs ref ->
-      Pretyping.var_map * (Names.identifier * Names.identifier option) list ->
-      Rawterm.rawconstr -> Environ.unsafe_type_judgment
-    val pretype_gen :
-      Evd.evar_defs ref ->
-      Environ.env ->
-      Pretyping.var_map * (Names.identifier * Names.identifier option) list ->
-      Pretyping.typing_constraint -> Rawterm.rawconstr -> Term.constr
-  end
+open Pretyping
+open Evd
+open Environ
+open Term
+open Topconstr
+open Names
+open Libnames
+open Pp
+open Vernacexpr
+open Constrintern
+
 val interp_gen :
-  Pretyping.typing_constraint ->
-  Evd.evar_defs ref ->
-  Environ.env ->
-  ?impls:Constrintern.full_implicits_env ->
+  typing_constraint ->
+  evar_defs ref ->
+  env ->
+  ?impls:full_implicits_env ->
   ?allow_soapp:bool ->
-  ?ltacvars:Constrintern.ltac_sign ->
-  Topconstr.constr_expr -> Evd.evar_map * Term.constr
+  ?ltacvars:ltac_sign ->
+  constr_expr -> evar_map * constr
 val interp_constr :
-  Evd.evar_defs ref ->
-  Environ.env -> Topconstr.constr_expr -> Evd.evar_map * Term.constr
+  evar_defs ref ->
+  env -> constr_expr -> evar_map * constr
 val interp_type :
-  Evd.evar_defs ref ->
-  Environ.env ->
-  ?impls:Constrintern.full_implicits_env ->
-  Topconstr.constr_expr -> Evd.evar_map * Term.constr
+  evar_defs ref ->
+  env ->
+  ?impls:full_implicits_env ->
+  constr_expr -> evar_map * constr
 val interp_casted_constr :
-  Evd.evar_defs ref ->
-  Environ.env ->
-  ?impls:Constrintern.full_implicits_env ->
-  Topconstr.constr_expr -> Term.types -> Evd.evar_map * Term.constr
+  evar_defs ref ->
+  env ->
+  ?impls:full_implicits_env ->
+  constr_expr -> types -> evar_map * constr
 val interp_open_constr :
-  Evd.evar_defs ref -> Environ.env -> Topconstr.constr_expr -> Term.constr
+  evar_defs ref -> env -> constr_expr -> constr
 val interp_constr_judgment :
-  Evd.evar_defs ref ->
-  Environ.env ->
-  Topconstr.constr_expr -> Evd.evar_defs * Environ.unsafe_judgment
+  evar_defs ref ->
+  env ->
+  constr_expr -> evar_defs * unsafe_judgment
 val list_chop_hd : int -> 'a list -> 'a list * 'a * 'a list
-val collect_non_rec :
-  Environ.env ->
-  Names.identifier list ->
-  ('a * Term.types) list ->
-  'b list ->
-  'c list ->
-  (Names.identifier * ('a * Term.types) * 'b) list *
-  (Names.identifier array * ('a * Term.types) array * 'b array * 'c array)
-val recursive_message : Libnames.global_reference array -> Pp.std_ppcmds
+val recursive_message : global_reference array -> std_ppcmds
 val build_recursive :
-  (Topconstr.fixpoint_expr * Vernacexpr.decl_notation) list -> bool -> unit
+  (fixpoint_expr * decl_notation) list -> bool -> unit