From 012fe1a96ba81ab0a7fa210610e3f25187baaf1d Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 12 Aug 2014 14:03:32 +0200 Subject: Referring to evars by names. Added a parser for evars (but parsing of instances still to do). Using heuristics to name after the quantifier name it comes. Also added a "sigma" to almost all printing functions. --- interp/reserve.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'interp/reserve.ml') diff --git a/interp/reserve.ml b/interp/reserve.ml index 272e6c8d1..33c21eea5 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -108,7 +108,7 @@ let constr_key c = let revert_reserved_type t = try let reserved = KeyMap.find (constr_key t) !reserve_revtable in - let t = Detyping.detype false [] [] t in + let t = Detyping.detype false [] [] Evd.empty t in (* pedrot: if [Notation_ops.match_notation_constr] may raise [Failure _] then I've introduced a bug... *) let filter _ pat = -- cgit v1.2.3