Indexing Proofview.goals with a stage.

This is not perfect though, some primitives are unsound, and some
higher-order API should use polymorphic functions so as not to depend
on a given level.

1 files changed, 23 insertions, 22 deletions

diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index a0e1a0157..3ed6a2eeb 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -106,36 +106,37 @@ val pr_glls   : goal list sigma -> Pp.std_ppcmds
 
 (* Variants of [Tacmach] functions built with the new proof engine *)
 module New : sig
-  val pf_apply : (env -> evar_map -> 'a) -> 'b Proofview.Goal.t -> 'a
-  val pf_global : identifier -> 'a Proofview.Goal.t -> constr
-  val of_old : (Proof_type.goal Evd.sigma -> 'a) -> [ `NF ] Proofview.Goal.t -> 'a
+  val pf_apply : (env -> evar_map -> 'a) -> ('b, 'r) Proofview.Goal.t -> 'a
+  val pf_global : identifier -> ('a, 'r) Proofview.Goal.t -> constr
+  (** FIXME: encapsulate the level in an existential type. *)
+  val of_old : (Proof_type.goal Evd.sigma -> 'a) -> ([ `NF ], 'r) Proofview.Goal.t -> 'a
 
-  val pf_env : 'a Proofview.Goal.t -> Environ.env
-  val pf_concl : [ `NF ] Proofview.Goal.t -> types
+  val pf_env : ('a, 'r) Proofview.Goal.t -> Environ.env
+  val pf_concl : ([ `NF ], 'r) Proofview.Goal.t -> types
 
-  val pf_unsafe_type_of : 'a Proofview.Goal.t -> Term.constr -> Term.types
-  val pf_type_of : 'a Proofview.Goal.t -> Term.constr -> evar_map * Term.types
-  val pf_conv_x : 'a Proofview.Goal.t -> Term.constr -> Term.constr -> bool
+  val pf_unsafe_type_of : ('a, 'r) Proofview.Goal.t -> Term.constr -> Term.types
+  val pf_type_of : ('a, 'r) Proofview.Goal.t -> Term.constr -> evar_map * Term.types
+  val pf_conv_x : ('a, 'r) Proofview.Goal.t -> Term.constr -> Term.constr -> bool
 
-  val pf_get_new_id  : identifier -> [ `NF ] Proofview.Goal.t -> identifier
-  val pf_ids_of_hyps : 'a Proofview.Goal.t -> identifier list
-  val pf_hyps_types : 'a Proofview.Goal.t -> (identifier * types) list
+  val pf_get_new_id  : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> identifier
+  val pf_ids_of_hyps : ('a, 'r) Proofview.Goal.t -> identifier list
+  val pf_hyps_types : ('a, 'r) Proofview.Goal.t -> (identifier * types) list
 
-  val pf_get_hyp : identifier -> [ `NF ] Proofview.Goal.t -> named_declaration
-  val pf_get_hyp_typ        : identifier -> [ `NF ] Proofview.Goal.t -> types
-  val pf_last_hyp           : [ `NF ] Proofview.Goal.t -> named_declaration
+  val pf_get_hyp : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> named_declaration
+  val pf_get_hyp_typ        : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> types
+  val pf_last_hyp           : ([ `NF ], 'r) Proofview.Goal.t -> named_declaration
 
-  val pf_nf_concl : [ `LZ ] Proofview.Goal.t -> types
-  val pf_reduce_to_quantified_ind : 'a Proofview.Goal.t -> types -> pinductive * types
+  val pf_nf_concl : ([ `LZ ], 'r) Proofview.Goal.t -> types
+  val pf_reduce_to_quantified_ind : ('a, 'r) Proofview.Goal.t -> types -> pinductive * types
 
-  val pf_hnf_constr : 'a Proofview.Goal.t -> constr -> types
-  val pf_hnf_type_of : 'a Proofview.Goal.t -> constr -> types
+  val pf_hnf_constr : ('a, 'r) Proofview.Goal.t -> constr -> types
+  val pf_hnf_type_of : ('a, 'r) Proofview.Goal.t -> constr -> types
 
-  val pf_whd_betadeltaiota : 'a Proofview.Goal.t -> constr -> constr
-  val pf_compute : 'a Proofview.Goal.t -> constr -> constr
+  val pf_whd_betadeltaiota : ('a, 'r) Proofview.Goal.t -> constr -> constr
+  val pf_compute : ('a, 'r) Proofview.Goal.t -> constr -> constr
 
-  val pf_matches : 'a Proofview.Goal.t -> constr_pattern -> constr -> patvar_map
+  val pf_matches : ('a, 'r) Proofview.Goal.t -> constr_pattern -> constr -> patvar_map
 
-  val pf_nf_evar : 'a Proofview.Goal.t -> constr -> constr
+  val pf_nf_evar : ('a, 'r) Proofview.Goal.t -> constr -> constr
 
 end