diff options
| author | herbelin | 2003-10-14 10:45:37 +0000 |
|---|---|---|
| committer | herbelin | 2003-10-14 10:45:37 +0000 |
| commit | 0deab676d514b5c544f054d4642252ccfa4c4e7a (patch) | |
| tree | 0facbc326cc6623e64fa9b0346e494800c013274 /interp/constrintern.mli | |
| parent | 029b01a914f7f3cfb615bbac8b86447b6216cf7e (diff) | |
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
Diffstat (limited to 'interp/constrintern.mli')
| -rw-r--r-- | interp/constrintern.mli | 14 |
1 files changed, 10 insertions, 4 deletions
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 |