diff options
| author | msozeau | 2008-05-06 14:05:20 +0000 |
|---|---|---|
| committer | msozeau | 2008-05-06 14:05:20 +0000 |
| commit | 7a39bd5650cc49c5c77788fb42fe2caaf35dfdac (patch) | |
| tree | 5303c8ae52d603314486350cdbfb5187eee089c5 /interp/constrintern.mli | |
| parent | 92fd77538371d96a52326eb73b120800c9fe79c9 (diff) | |
Postpone the search for the recursive argument index from the user given
name after internalisation, to get the correct behavior with typeclass
binders. This simplifies the pretty printing and translation
of the recursive argument name in various places too. Use this
opportunity to factorize the different internalization and
interpretation functions of binders as well.
This definitely fixes part 2 of bug
#1846 and makes it possible to use fixpoint definitions with typeclass arguments in
program too, with an example given in EquivDec.
At the same time, one fix and one enhancement in Program:
- fix a de Bruijn bug in subtac_cases
- introduce locations of obligations and use them in case the obligation tactic
raises a failure when tried on a particular obligation, as suggested by
Sean Wilson.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10889 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/constrintern.mli')
| -rw-r--r-- | interp/constrintern.mli | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/interp/constrintern.mli b/interp/constrintern.mli index f81b2ccd16..fb69460c4a 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -49,6 +49,8 @@ type manual_implicits = (explicitation * (bool * bool)) list type ltac_sign = identifier list * unbound_ltac_var_map +type raw_binder = (name * binding_kind * rawconstr option * rawconstr) + (*s Internalisation performs interpretation of global names and notations *) val intern_constr : evar_map -> env -> constr_expr -> rawconstr @@ -63,6 +65,8 @@ val intern_pattern : env -> cases_pattern_expr -> Names.identifier list * ((Names.identifier * Names.identifier) list * Rawterm.cases_pattern) list +val intern_context : evar_map -> env -> local_binder list -> raw_binder list + (*s Composing internalisation with pretyping *) (* Main interpretation function *) @@ -120,10 +124,10 @@ val interp_binder_evars : evar_defs ref -> env -> name -> constr_expr -> types (* Interpret contexts: returns extended env and context *) -val interp_context : evar_map -> env -> local_binder list -> env * rel_context +val interp_context : evar_map -> env -> local_binder list -> (env * rel_context) * manual_implicits val interp_context_evars : - evar_defs ref -> env -> local_binder list -> env * rel_context + evar_defs ref -> env -> local_binder list -> (env * rel_context) * manual_implicits (* Locating references of constructions, possibly via a syntactic definition *) |