From 84544396cbbf34848be2240acf181b4d5f1f42d2 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Sat, 27 Sep 2014 16:08:02 +0200 Subject: Add a boolean to indicate the unfolding state of a primitive projection, so as to reproduce correctly the reduction behavior of existing projections, i.e. delta + iota. Make [projection] an abstract datatype in Names.ml, most of the patch is about using that abstraction. Fix unification.ml which tried canonical projections too early in presence of primitive projections. --- pretyping/patternops.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'pretyping/patternops.mli') diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli index cfe71510a..382357a8d 100644 --- a/pretyping/patternops.mli +++ b/pretyping/patternops.mli @@ -39,7 +39,7 @@ val head_of_constr_reference : Term.constr -> global_reference a pattern; currently, no destructor (Cases, Fix, Cofix) and no existential variable are allowed in [c] *) -val pattern_of_constr : Evd.evar_map -> constr -> named_context * constr_pattern +val pattern_of_constr : Environ.env -> Evd.evar_map -> constr -> named_context * constr_pattern (** [pattern_of_glob_constr l c] translates a term [c] with metavariables into a pattern; variables bound in [l] are replaced by the pattern to which they @@ -48,7 +48,7 @@ val pattern_of_constr : Evd.evar_map -> constr -> named_context * constr_pattern val pattern_of_glob_constr : glob_constr -> patvar list * constr_pattern -val instantiate_pattern : +val instantiate_pattern : Environ.env -> Evd.evar_map -> extended_patvar_map -> constr_pattern -> constr_pattern -- cgit v1.2.3