aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.depend54
-rw-r--r--kernel/environ.mli12
-rw-r--r--kernel/safe_typing.mli8
-rw-r--r--kernel/sign.mli8
-rw-r--r--kernel/term.mli2
-rw-r--r--kernel/typeops.mli4
-rw-r--r--library/global.mli6
-rw-r--r--parsing/g_minicoq.ml44
-rw-r--r--parsing/g_minicoq.mli4
-rw-r--r--proofs/logic.mli17
-rw-r--r--proofs/tacinterp.mli2
-rw-r--r--proofs/tacmach.mli2
-rw-r--r--tactics/tacentries.mli2
-rw-r--r--tactics/tacticals.mli8
-rw-r--r--toplevel/fhimsg.ml36
-rw-r--r--toplevel/fhimsg.mli30
-rw-r--r--toplevel/minicoq.ml7
17 files changed, 109 insertions, 97 deletions
diff --git a/.depend b/.depend
index 3e97c1667d..ba4d941ee6 100644
--- a/.depend
+++ b/.depend
@@ -32,6 +32,8 @@ kernel/typeops.cmi: kernel/environ.cmi kernel/evd.cmi kernel/inductive.cmi \
kernel/names.cmi kernel/sign.cmi kernel/term.cmi kernel/univ.cmi
kernel/univ.cmi: kernel/names.cmi lib/pp.cmi
lib/pp.cmi: lib/pp_control.cmi
+lib/system.cmi: lib/pp.cmi
+lib/util.cmi: lib/pp.cmi
library/declare.cmi: kernel/declarations.cmi kernel/environ.cmi \
kernel/inductive.cmi kernel/names.cmi kernel/sign.cmi kernel/term.cmi
library/global.cmi: kernel/declarations.cmi kernel/environ.cmi \
@@ -47,8 +49,6 @@ library/library.cmi: lib/pp.cmi
library/nametab.cmi: kernel/names.cmi
library/redinfo.cmi: kernel/names.cmi kernel/term.cmi
library/summary.cmi: kernel/names.cmi
-lib/system.cmi: lib/pp.cmi
-lib/util.cmi: lib/pp.cmi
parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \
parsing/pcoq.cmi lib/pp.cmi
parsing/astterm.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \
@@ -187,11 +187,11 @@ toplevel/record.cmi: parsing/coqast.cmi kernel/names.cmi kernel/term.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 \
toplevel/vernacinterp.cmi
toplevel/vernacinterp.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \
proofs/proof_type.cmi
-toplevel/vernac.cmi: parsing/coqast.cmi parsing/pcoq.cmi
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
@@ -318,22 +318,30 @@ lib/dyn.cmo: lib/util.cmi lib/dyn.cmi
lib/dyn.cmx: lib/util.cmx lib/dyn.cmi
lib/edit.cmo: lib/bstack.cmi lib/pp.cmi lib/util.cmi lib/edit.cmi
lib/edit.cmx: lib/bstack.cmx lib/pp.cmx lib/util.cmx lib/edit.cmi
-lib/gmapl.cmo: lib/gmap.cmi lib/util.cmi lib/gmapl.cmi
-lib/gmapl.cmx: lib/gmap.cmx lib/util.cmx lib/gmapl.cmi
lib/gmap.cmo: lib/gmap.cmi
lib/gmap.cmx: lib/gmap.cmi
+lib/gmapl.cmo: lib/gmap.cmi lib/util.cmi lib/gmapl.cmi
+lib/gmapl.cmx: lib/gmap.cmx lib/util.cmx lib/gmapl.cmi
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/util.cmi lib/options.cmi
lib/options.cmx: lib/util.cmx lib/options.cmi
-lib/pp_control.cmo: lib/pp_control.cmi
-lib/pp_control.cmx: lib/pp_control.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
+lib/pp_control.cmx: lib/pp_control.cmi
lib/profile.cmo: lib/system.cmi lib/profile.cmi
lib/profile.cmx: lib/system.cmx lib/profile.cmi
+lib/stamps.cmo: lib/stamps.cmi
+lib/stamps.cmx: lib/stamps.cmi
+lib/system.cmo: lib/pp.cmi lib/util.cmi lib/system.cmi
+lib/system.cmx: lib/pp.cmx lib/util.cmx lib/system.cmi
+lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi
+lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi
+lib/util.cmo: lib/pp.cmi lib/util.cmi
+lib/util.cmx: lib/pp.cmx lib/util.cmi
library/declare.cmo: kernel/declarations.cmi kernel/environ.cmi \
kernel/evd.cmi kernel/generic.cmi library/global.cmi library/impargs.cmi \
library/indrec.cmi kernel/inductive.cmi library/lib.cmi \
@@ -410,14 +418,6 @@ library/summary.cmo: lib/dyn.cmi kernel/names.cmi lib/pp.cmi lib/util.cmi \
library/summary.cmi
library/summary.cmx: lib/dyn.cmx kernel/names.cmx lib/pp.cmx lib/util.cmx \
library/summary.cmi
-lib/stamps.cmo: lib/stamps.cmi
-lib/stamps.cmx: lib/stamps.cmi
-lib/system.cmo: lib/pp.cmi lib/util.cmi lib/system.cmi
-lib/system.cmx: lib/pp.cmx lib/util.cmx lib/system.cmi
-lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi
-lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi
-lib/util.cmo: lib/pp.cmi lib/util.cmi
-lib/util.cmx: lib/pp.cmx lib/util.cmi
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 \
@@ -994,8 +994,12 @@ tactics/wcclausenv.cmx: proofs/clenv.cmx kernel/environ.cmx kernel/evd.cmx \
lib/pp.cmx proofs/proof_trees.cmx kernel/reduction.cmx \
pretyping/retyping.cmx kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx \
lib/util.cmx tactics/wcclausenv.cmi
-tools/coqdep.cmo: config/coq_config.cmi
-tools/coqdep.cmx: config/coq_config.cmx
+tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo
+tools/coqdep.cmx: config/coq_config.cmx tools/coqdep_lexer.cmx
+tools/coqdep_lexer.cmo: config/coq_config.cmi
+tools/coqdep_lexer.cmx: config/coq_config.cmx
+tools/gallina.cmo: tools/gallina_lexer.cmo
+tools/gallina.cmx: tools/gallina_lexer.cmx
toplevel/command.cmo: parsing/ast.cmi parsing/astterm.cmi parsing/coqast.cmi \
kernel/declarations.cmi library/declare.cmi kernel/environ.cmi \
kernel/evd.cmi kernel/generic.cmi library/global.cmi library/indrec.cmi \
@@ -1114,6 +1118,14 @@ toplevel/toplevel.cmx: parsing/ast.cmx toplevel/errors.cmx toplevel/mltop.cmi \
toplevel/vernac.cmx toplevel/vernacinterp.cmx toplevel/toplevel.cmi
toplevel/usage.cmo: toplevel/usage.cmi
toplevel/usage.cmx: toplevel/usage.cmi
+toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi library/library.cmi \
+ lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.cmi \
+ library/states.cmi lib/system.cmi lib/util.cmi toplevel/vernacinterp.cmi \
+ toplevel/vernac.cmi
+toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/library.cmx \
+ lib/options.cmx parsing/pcoq.cmx 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 parsing/astterm.cmi \
pretyping/class.cmi toplevel/command.cmi parsing/coqast.cmi \
library/declare.cmi toplevel/discharge.cmi kernel/environ.cmi \
@@ -1150,14 +1162,6 @@ toplevel/vernacinterp.cmx: parsing/ast.cmx toplevel/command.cmx \
parsing/coqast.cmx lib/dyn.cmx toplevel/himsg.cmx kernel/names.cmx \
lib/options.cmx lib/pp.cmx proofs/proof_type.cmx proofs/tacinterp.cmx \
lib/util.cmx toplevel/vernacinterp.cmi
-toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi library/library.cmi \
- lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.cmi \
- library/states.cmi lib/system.cmi lib/util.cmi toplevel/vernacinterp.cmi \
- toplevel/vernac.cmi
-toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/library.cmx \
- lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx lib/pp.cmx \
- library/states.cmx lib/system.cmx lib/util.cmx toplevel/vernacinterp.cmx \
- toplevel/vernac.cmi
contrib/omega/coq_omega.cmo: parsing/ast.cmi proofs/clenv.cmi \
library/declare.cmi kernel/environ.cmi tactics/equality.cmi \
kernel/generic.cmi library/global.cmi kernel/inductive.cmi \
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 616a111620..981be607fc 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -49,21 +49,21 @@ val names_of_rel_context : env -> names_context
(*s Returns also the substitution to be applied to rel's *)
val push_rels_to_vars : env -> constr list * env
-(* Gives identifiers in var_context and rel_context *)
+(* Gives identifiers in [var_context] and [rel_context] *)
val ids_of_context : env -> identifier list
val map_context : (constr -> constr) -> env -> env
-(*s Recurrence on var_context *)
+(*s Recurrence on [var_context] *)
val fold_var_context : (env -> var_declaration -> 'a -> 'a) -> env -> 'a -> 'a
val process_var_context : (env -> var_declaration -> env) -> env -> env
(* [process_var_context_both_sides f env] iters [f] on the var
- declarations of env taking as argument both the initial segment, the
+ declarations of [env] taking as argument both the initial segment, the
middle value and the tail segment *)
val process_var_context_both_sides :
(env -> var_declaration -> var_context -> env) -> env -> env
-(*s Recurrence on rel_context *)
+(*s Recurrence on [rel_context] *)
val fold_rel_context : (env -> rel_declaration -> 'a -> 'a) -> env -> 'a -> 'a
val process_rel_context : (env -> rel_declaration -> env) -> env -> env
@@ -81,13 +81,13 @@ val new_meta : unit -> int
(*s Looks up in environment *)
-(* Looks up in the context of local vars referred by names (var_context) *)
+(* Looks up in the context of local vars referred by names ([var_context]) *)
(* raises [Not_found] if the identifier is not found *)
val lookup_var_type : identifier -> env -> typed_type
val lookup_var_value : identifier -> env -> constr option
val lookup_var : identifier -> env -> constr option * typed_type
-(* Looks up in the context of local vars referred by indice (rel_context) *)
+(* Looks up in the context of local vars referred by indice ([rel_context]) *)
(* raises [Not_found] if the index points out of the context *)
val lookup_rel_type : int -> env -> name * typed_type
val lookup_rel_value : int -> env -> constr option
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 6d8c80bd0d..c2fb4a3c09 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -28,10 +28,10 @@ val var_context : safe_environment -> var_context
val push_var_decl : identifier * constr -> safe_environment -> safe_environment
val push_var_def : identifier * constr -> safe_environment -> safe_environment
-(*
+(*i
val push_rel_decl : name * constr -> safe_environment -> safe_environment
val push_rel_def : name * constr -> safe_environment -> safe_environment
-*)
+i*)
val add_constant :
section_path -> constant_entry -> safe_environment -> safe_environment
@@ -48,9 +48,9 @@ val add_constraints : constraints -> safe_environment -> safe_environment
val pop_vars : identifier list -> safe_environment -> safe_environment
val lookup_var : identifier -> safe_environment -> constr option * typed_type
-(*
+(*i
val lookup_rel : int -> safe_environment -> name * typed_type
-*)
+i*)
val lookup_constant : section_path -> safe_environment -> constant_body
val lookup_mind : section_path -> safe_environment -> mutual_inductive_body
val lookup_mind_specif : inductive -> safe_environment -> inductive_instance
diff --git a/kernel/sign.mli b/kernel/sign.mli
index 3add55894c..17d9267d98 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -7,13 +7,15 @@ open Generic
open Term
(*i*)
-(*s Signatures of _ordered_ named variables, intended to be accessed by name *)
+(*s Signatures of ordered named variables, intended to be accessed by name *)
type var_context = var_declaration list
-val add_var : identifier * constr option * typed_type -> var_context -> var_context
+val add_var :
+ identifier * constr option * typed_type -> var_context -> var_context
val add_var_decl : identifier * typed_type -> var_context -> var_context
-val add_var_def : identifier * constr * typed_type -> var_context ->var_context
+val add_var_def :
+ identifier * constr * typed_type -> var_context -> var_context
val lookup_id : identifier -> var_context -> constr option * typed_type
val lookup_id_type : identifier -> var_context -> typed_type
val lookup_id_value : identifier -> var_context -> constr option
diff --git a/kernel/term.mli b/kernel/term.mli
index 9019fa091f..cd86af6756 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -100,7 +100,7 @@ type 'ctxt reference =
(* Concrete type for making pattern-matching. *)
-(* [constr array] is an instance matching definitional var_context in
+(* [constr array] is an instance matching definitional [var_context] in
the same order (i.e. last argument first) *)
type existential = int * constr array
type constant = section_path * constr array
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index a07206fb0f..a2fedf7f16 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -84,7 +84,7 @@ open Inductive
val find_case_dep_nparams :
env -> 'a evar_map -> constr * constr -> inductive_family -> constr -> bool
-(*
+(*i
val hyps_inclusion : env -> 'a evar_map -> var_context -> var_context -> bool
-*)
+i*)
diff --git a/library/global.mli b/library/global.mli
index c2e8ac386c..b51ce3c774 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -25,11 +25,11 @@ val var_context : unit -> var_context
val push_var_decl : identifier * constr -> unit
val push_var_def : identifier * constr -> unit
-(*
+(*i
val push_var : identifier * constr option * constr -> unit
val push_rel_decl : name * constr -> unit
val push_rel_def : name * constr -> unit
-*)
+i*)
val add_constant : section_path -> constant_entry -> unit
val add_parameter : section_path -> constr -> unit
val add_mind : section_path -> mutual_inductive_entry -> unit
@@ -38,7 +38,7 @@ val add_constraints : constraints -> unit
val pop_vars : identifier list -> unit
val lookup_var : identifier -> constr option * typed_type
-(*val lookup_rel : int -> name * typed_type*)
+(*i val lookup_rel : int -> name * typed_type i*)
val lookup_constant : section_path -> constant_body
val lookup_mind : section_path -> mutual_inductive_body
val lookup_mind_specif : inductive -> inductive_instance
diff --git a/parsing/g_minicoq.ml4 b/parsing/g_minicoq.ml4
index c14c5d0344..21163804ec 100644
--- a/parsing/g_minicoq.ml4
+++ b/parsing/g_minicoq.ml4
@@ -7,7 +7,7 @@ open Names
open Univ
open Generic
open Term
-open Sign
+open Environ
let lexer = {
Token.func = Lexer.func;
@@ -176,5 +176,5 @@ let rec pp bv = function
| Rel n -> print_rel bv n
| _ -> [< 'sTR"<???>" >]
-let pr_term _ ctx = pp (it_dbenv (fun l n _ -> n::l) [] ctx)
+let pr_term _ ctx = pp (fold_rel_context (fun _ (n,_,_) l -> n::l) ctx [])
diff --git a/parsing/g_minicoq.mli b/parsing/g_minicoq.mli
index de3a022862..db5c0d07f5 100644
--- a/parsing/g_minicoq.mli
+++ b/parsing/g_minicoq.mli
@@ -3,7 +3,7 @@
open Pp
open Names
open Term
-open Sign
+open Environ
(*i*)
val term : constr Grammar.Entry.e
@@ -19,4 +19,4 @@ type command =
val command : command Grammar.Entry.e
-val pr_term : path_kind -> context -> constr -> std_ppcmds
+val pr_term : path_kind -> env -> constr -> std_ppcmds
diff --git a/proofs/logic.mli b/proofs/logic.mli
index dd27797254..9247d4ff6e 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -10,20 +10,19 @@ open Environ
open Proof_type
(*i*)
-(* This suppresses check done in prim_refiner for the tactic given in
+(* This suppresses check done in [prim_refiner] for the tactic given in
argument; works by side-effect *)
val without_check : tactic -> tactic
-(* without_check respectively means:\\
-\\
- Intro: no check that the name does not exist\\
- Intro_after: no check that the name does not exist and that variables in
+(* [without_check] respectively means:\\
+ [Intro]: no check that the name does not exist\\
+ [Intro_after]: no check that the name does not exist and that variables in
its type does not escape their scope\\
- Intro_replacing: no check that the name does not exist and that variables in
- its type does not escape their scope\\
-
- Convert_hyp: no check that the name exist and that its type is convertible\\
+ [Intro_replacing]: no check that the name does not exist and that
+ variables in its type does not escape their scope\\
+ [Convert_hyp]:
+ no check that the name exist and that its type is convertible\\
*)
(* The primitive refiner. *)
diff --git a/proofs/tacinterp.mli b/proofs/tacinterp.mli
index 39351dc1e5..50b454df8f 100644
--- a/proofs/tacinterp.mli
+++ b/proofs/tacinterp.mli
@@ -37,7 +37,7 @@ val val_interp : interp_sign -> Coqast.t -> value
val interp_tacarg : interp_sign -> Coqast.t -> tactic_arg
val interp : Coqast.t -> tactic
-(*val vernac_interp : Coqast.t -> tactic*)
+(*i val vernac_interp : Coqast.t -> tactic i*)
val vernac_interp_atomic : identifier -> tactic_arg list -> tactic
val is_just_undef_macro : Coqast.t -> string option
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 6ae4f9ae26..bf2b0a3bab 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -34,7 +34,7 @@ val apply_sig_tac :
val pf_concl : goal sigma -> constr
val pf_env : goal sigma -> env
val pf_hyps : goal sigma -> var_context
-(*val pf_untyped_hyps : goal sigma -> (identifier * constr) list*)
+(*i val pf_untyped_hyps : goal sigma -> (identifier * constr) list i*)
val pf_hyps_types : goal sigma -> (identifier * constr) list
val pf_nth_hyp_id : goal sigma -> int -> identifier
val pf_last_hyp : goal sigma -> var_declaration
diff --git a/tactics/tacentries.mli b/tactics/tacentries.mli
index 6efd48d555..b364706ca1 100644
--- a/tactics/tacentries.mli
+++ b/tactics/tacentries.mli
@@ -15,7 +15,7 @@ val v_symmetry : tactic_arg list -> tactic
val v_transitivity : tactic_arg list -> tactic
val v_intro : tactic_arg list -> tactic
val v_introsUntil : tactic_arg list -> tactic
-(*val v_tclIDTAC : tactic_arg list -> tactic*)
+(*i val v_tclIDTAC : tactic_arg list -> tactic i*)
val v_assumption : tactic_arg list -> tactic
val v_exact : tactic_arg list -> tactic
val v_reduce : tactic_arg list -> tactic
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 0cdedd8c68..4b89938276 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -37,8 +37,10 @@ val tclLAST_HYP : (constr -> tactic) -> tactic
val tclTRY_sign : (constr -> tactic) -> var_context -> tactic
val tclTRY_HYPS : (constr -> tactic) -> tactic
-(*val dyn_tclIDTAC : tactic_arg list -> tactic
-val dyn_tclFAIL : tactic_arg list -> tactic*)
+(*i
+val dyn_tclIDTAC : tactic_arg list -> tactic
+val dyn_tclFAIL : tactic_arg list -> tactic
+i*)
(*s Clause tacticals. *)
@@ -103,7 +105,7 @@ type branch_assumptions = {
indargs : identifier list} (* the inductive arguments *)
val sort_of_goal : goal sigma -> sorts
-(*val suff : goal sigma -> constr -> string*)
+(*i val suff : goal sigma -> constr -> string i*)
val general_elim_then_using :
constr -> (inductive -> int -> bool list) ->
diff --git a/toplevel/fhimsg.ml b/toplevel/fhimsg.ml
index dcc0a86976..9d0e9558a6 100644
--- a/toplevel/fhimsg.ml
+++ b/toplevel/fhimsg.ml
@@ -13,13 +13,13 @@ open Reduction
open G_minicoq
module type Printer = sig
- val pr_term : path_kind -> context -> constr -> std_ppcmds
+ val pr_term : path_kind -> env -> constr -> std_ppcmds
end
module Make = functor (P : Printer) -> struct
- let print_decl k sign (s,typ) =
- let ptyp = P.pr_term k (gLOB sign) (body_of_type typ) in
+ let print_decl k env (s,typ) =
+ let ptyp = P.pr_term k env (body_of_type typ) in
[< 'sPC; print_id s; 'sTR" : "; ptyp >]
let print_binding k env = function
@@ -28,34 +28,38 @@ module Make = functor (P : Printer) -> struct
| Name id,ty ->
[< 'sPC; print_id id ; 'sTR" : "; P.pr_term k env (body_of_type ty) >]
+(****
let sign_it_with f sign e =
- snd (sign_it
- (fun id t (sign,e) -> (add_sign (id,t) sign, f id t sign e))
- sign (nil_sign,e))
+ snd (fold_var_context
+ (fun (id,v,t) (sign,e) -> (add_var (id,v,t) sign, f id t sign e))
+ sign (empty_var_context,e))
let dbenv_it_with f env e =
snd (dbenv_it
(fun na t (env,e) -> (add_rel (na,t) env, f na t env e))
env (gLOB(get_globals env),e))
+****)
let pr_env k env =
let sign_env =
- sign_it_with
- (fun id t sign pps ->
- let pidt = print_decl k sign (id,t) in [< pps ; 'fNL ; pidt >])
- (get_globals env) [< >]
+ fold_var_context
+ (fun env (id,_,t) pps ->
+ let pidt = print_decl k env (id,t) in [< pps ; 'fNL ; pidt >])
+ env [< >]
in
let db_env =
- dbenv_it_with
- (fun na t env pps ->
+ fold_rel_context
+ (fun env (na,_,t) pps ->
let pnat = print_binding k env (na,t) in [< pps ; 'fNL ; pnat >])
env [< >]
in
[< sign_env; db_env >]
- let pr_ne_ctx header k = function
- | ENVIRON (s1,s2) when s1=nil_sign & s2=nil_dbsign -> [< >]
- | env -> [< header; pr_env k env >]
+ let pr_ne_ctx header k env =
+ if rel_context env = [] && var_context env = [] then
+ [< >]
+ else
+ [< header; pr_env k env >]
let explain_unbound_rel k ctx n =
@@ -129,7 +133,7 @@ let explain_ill_formed_branch k ctx c i actty expty =
let explain_generalization k ctx (name,var) c =
let pe = pr_ne_ctx [< 'sTR"in environment" >] k ctx in
let pv = P.pr_term k ctx (body_of_type var) in
- let pc = P.pr_term k (add_rel (name,var) ctx) c in
+ let pc = P.pr_term k (push_rel (name,None,var) ctx) c in
[< 'sTR"Illegal generalization: "; pe; 'fNL;
'sTR"Cannot generalize"; 'bRK(1,1); pv; 'sPC;
'sTR"over"; 'bRK(1,1); pc; 'sPC;
diff --git a/toplevel/fhimsg.mli b/toplevel/fhimsg.mli
index eb8d615538..ad0e7e6646 100644
--- a/toplevel/fhimsg.mli
+++ b/toplevel/fhimsg.mli
@@ -15,53 +15,53 @@ open Type_errors
context. *)
module type Printer = sig
- val pr_term : path_kind -> context -> constr -> std_ppcmds
+ val pr_term : path_kind -> env -> constr -> std_ppcmds
end
(*s The result is a module which provides a function [explain_type_error]
- to explain a type error for a given kind in a given context, which are
+ to explain a type error for a given kind in a given env, which are
usually the three arguments carried by the exception [TypeError]
(see \refsec{typeerrors}). *)
module Make (P : Printer) : sig
-val explain_type_error : path_kind -> context -> type_error -> std_ppcmds
+val explain_type_error : path_kind -> env -> type_error -> std_ppcmds
-val pr_ne_ctx : std_ppcmds -> path_kind -> context -> std_ppcmds
+val pr_ne_ctx : std_ppcmds -> path_kind -> env -> std_ppcmds
-val explain_unbound_rel : path_kind -> context -> int -> std_ppcmds
+val explain_unbound_rel : path_kind -> env -> int -> std_ppcmds
-val explain_not_type : path_kind -> context -> constr -> std_ppcmds
+val explain_not_type : path_kind -> env -> constr -> std_ppcmds
-val explain_bad_assumption : path_kind -> context -> constr -> std_ppcmds
+val explain_bad_assumption : path_kind -> env -> constr -> std_ppcmds
val explain_reference_variables : identifier -> std_ppcmds
val explain_elim_arity :
- path_kind -> context -> constr -> constr list -> constr
+ path_kind -> env -> constr -> constr list -> constr
-> constr -> constr -> (constr * constr * string) option -> std_ppcmds
val explain_case_not_inductive :
- path_kind -> context -> constr -> constr -> std_ppcmds
+ path_kind -> env -> constr -> constr -> std_ppcmds
val explain_number_branches :
- path_kind -> context -> constr -> constr -> int -> std_ppcmds
+ path_kind -> env -> constr -> constr -> int -> std_ppcmds
val explain_ill_formed_branch :
- path_kind -> context -> constr -> int -> constr -> constr -> std_ppcmds
+ path_kind -> env -> constr -> int -> constr -> constr -> std_ppcmds
val explain_generalization :
- path_kind -> context -> name * typed_type -> constr -> std_ppcmds
+ path_kind -> env -> name * typed_type -> constr -> std_ppcmds
val explain_actual_type :
- path_kind -> context -> constr -> constr -> constr -> std_ppcmds
+ path_kind -> env -> constr -> constr -> constr -> std_ppcmds
val explain_ill_formed_rec_body :
- path_kind -> context -> std_ppcmds ->
+ path_kind -> env -> std_ppcmds ->
name list -> int -> constr array -> std_ppcmds
val explain_ill_typed_rec_body :
- path_kind -> context -> int -> name list -> unsafe_judgment array
+ path_kind -> env -> int -> name list -> unsafe_judgment array
-> typed_type array -> std_ppcmds
end
diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml
index 59253eb072..5df900c264 100644
--- a/toplevel/minicoq.ml
+++ b/toplevel/minicoq.ml
@@ -23,7 +23,8 @@ let lookup_var id =
in
look 1
-let args sign = Array.of_list (List.map (fun id -> VAR id) (ids_of_sign sign))
+let args sign =
+ Array.of_list (List.map (fun id -> VAR id) (ids_of_var_context sign))
let rec globalize bv = function
| VAR id -> lookup_var id bv
@@ -45,7 +46,7 @@ let check c =
let c = globalize [] c in
let (j,u) = safe_machine !env c in
let ty = j_type j in
- let pty = pr_term CCI (context !env) ty in
+ let pty = pr_term CCI (env_of_safe_env !env) ty in
mSGNL (hOV 0 [< 'sTR" :"; 'sPC; hOV 0 pty; 'fNL >])
let definition id ty c =
@@ -65,7 +66,7 @@ let parameter id t =
let variable id t =
let t = globalize [] t in
- env := push_var (id,t) !env;
+ env := push_var_decl (id,t) !env;
mSGNL (hOV 0 [< 'sTR"variable"; 'sPC; print_id id;
'sPC; 'sTR"is declared"; 'fNL >])
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:04:07 +0000