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/whelp.ml4 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'toplevel/whelp.ml4') diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4 index 32f2473c5..c8054cf43 100644 --- a/toplevel/whelp.ml4 +++ b/toplevel/whelp.ml4 @@ -177,7 +177,7 @@ let send_whelp req s = let _ = CUnix.run_command ~hook:print_string command in () let whelp_constr req c = - let c = detype false [whelm_special] [] c in + let c = detype false [whelm_special] [] Evd.empty c in send_whelp req (make_string uri_of_constr c) let whelp_constr_expr req c = -- cgit v1.2.3