From 83e0cb59ed9a07bdf0154aaa2169bc94acf88c19 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 27 Mar 2018 02:37:19 +0200
Subject: Swapping Context and Constr: defining declarations on constr in
 Constr.

This shall eventually allow to use contexts of declarations in the
definition of the "Case" constructor.

Basically, this means that Constr now includes Context and that the
"t" types of Context which were specialized on constr are not defined
in Constr (unfortunately using a heavy boilerplate).
---
 vernac/comFixpoint.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'vernac/comFixpoint.mli')

diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index f51bfbad59..b1a9c8a5a3 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -82,12 +82,12 @@ val interp_fixpoint :
 val declare_fixpoint :
   locality -> polymorphic ->
   recursive_preentry * UState.universe_decl * UState.t *
-  (Context.Rel.t * Impargs.manual_implicits * int option) list ->
+  (Constr.rel_context * Impargs.manual_implicits * int option) list ->
   Proof_global.lemma_possible_guards -> decl_notation list -> unit
 
 val declare_cofixpoint : locality -> polymorphic ->
   recursive_preentry * UState.universe_decl * UState.t *
-  (Context.Rel.t * Impargs.manual_implicits * int option) list ->
+  (Constr.rel_context * Impargs.manual_implicits * int option) list ->
   decl_notation list -> unit
 
 (** Very private function, do not use *)
-- 
cgit v1.2.3