From 0deab676d514b5c544f054d4642252ccfa4c4e7a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 14 Oct 2003 10:45:37 +0000
Subject: Plus d'uniformite dans la gestion des implicites d'inductifs;
 nouvelles entrees pour Metasyntax

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4631 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/constrintern.mli | 14 ++++++++++----
 1 file changed, 10 insertions(+), 4 deletions(-)

(limited to 'interp/constrintern.mli')

diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index fa71624358..c1c9ede029 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -33,10 +33,12 @@ open Termops
    - insert existential variables for implicit arguments
 *)
 
-type implicits_env = (* For interpretation of inductive type with implicits *)
-    identifier list * 
+type implicits_env = (* To interpret inductive type with implicits *)
     (identifier * (identifier list * Impargs.implicits_list)) list
 
+type full_implicits_env =
+    identifier list * implicits_env
+
 type ltac_sign = 
   identifier list * (identifier * identifier option) list
 
@@ -62,7 +64,10 @@ val interp_casted_openconstr    :
    argument associates a list of implicit positions to identifiers
    declared in the rel_context of [env] *)
 val interp_type_with_implicits : 
-  evar_map -> env -> implicits_env -> constr_expr -> types
+  evar_map -> env -> full_implicits_env -> constr_expr -> types
+
+val interp_rawconstr_with_implicits :
+  env -> identifier list -> implicits_env -> constr_expr -> rawconstr
 
 (*s Build a judgement from *)
 val judgment_of_rawconstr : evar_map -> env -> constr_expr -> unsafe_judgment
@@ -91,7 +96,8 @@ val interp_constrpattern :
 val interp_reference : ltac_sign -> reference -> rawconstr
 
 (* Interprets into a abbreviatable constr *)
-val interp_aconstr : identifier list -> constr_expr -> interpretation
+val interp_aconstr : implicits_env -> identifier list -> constr_expr ->
+  interpretation
 
 (* Globalization leak for Grammar *)
 val for_grammar : ('a -> 'b) -> 'a -> 'b
-- 
cgit v1.2.3