diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/tacred.ml | 19 | ||||
| -rw-r--r-- | pretyping/tacred.mli | 15 |
2 files changed, 34 insertions, 0 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index c705ac16e7..411fb0cd89 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -43,6 +43,25 @@ exception ReductionTacticError of reduction_tactic_error exception Elimconst exception Redelimination +type evaluable_global_reference = + | EvalVarRef of Id.t + | EvalConstRef of Constant.t + +(* Better to have it here that in closure, since used in grammar.cma *) +let eq_egr e1 e2 = match e1, e2 with + EvalConstRef con1, EvalConstRef con2 -> Constant.CanOrd.equal con1 con2 + | EvalVarRef id1, EvalVarRef id2 -> Id.equal id1 id2 + | _, _ -> false + +(* Here the semantics is completely unclear. + What does "Hint Unfold t" means when "t" is a parameter? + Does the user mean "Unfold X.t" or does she mean "Unfold y" + where X.t is later on instantiated with y? I choose the first + interpretation (i.e. an evaluable reference is never expanded). *) +let subst_evaluable_reference subst = function + | EvalVarRef id -> EvalVarRef id + | EvalConstRef kn -> EvalConstRef (Mod_subst.subst_constant subst kn) + let error_not_evaluable r = user_err ~hdr:"error_not_evaluable" (str "Cannot coerce" ++ spc () ++ Nametab.pr_global_env Id.Set.empty r ++ diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index 65e3421736..aa232175bb 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -18,6 +18,21 @@ open Locus open Univ open Ltac_pretype +(* XXX: Move to a module *) +type evaluable_global_reference = + | EvalVarRef of Id.t + | EvalConstRef of Constant.t + +val eq_egr : evaluable_global_reference -> evaluable_global_reference -> bool + +(** Here the semantics is completely unclear. + What does "Hint Unfold t" means when "t" is a parameter? + Does the user mean "Unfold X.t" or does she mean "Unfold y" + where X.t is later on instantiated with y? I choose the first + interpretation (i.e. an evaluable reference is never expanded). *) +val subst_evaluable_reference : + Mod_subst.substitution -> evaluable_global_reference -> evaluable_global_reference + type reduction_tactic_error = InvalidAbstraction of env * evar_map * constr * (env * Type_errors.type_error) |