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. --- toplevel/command.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'toplevel/command.ml') diff --git a/toplevel/command.ml b/toplevel/command.ml index 115c245f3..df07026f6 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -845,7 +845,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation = let error () = user_err_loc (constr_loc r, "Command.build_wellfounded", - Printer.pr_constr_env env rel ++ str " is not an homogeneous binary relation.") + Printer.pr_constr_env env !evdref rel ++ str " is not an homogeneous binary relation.") in try let ctx, ar = Reductionops.splay_prod_n env !evdref 2 relty in -- cgit v1.2.3