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. --- plugins/firstorder/sequent.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/firstorder/sequent.ml') diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 43bb6dbbf..afa178832 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -231,7 +231,7 @@ let extend_with_auto_hints l seq gl= let print_cmap map= let print_entry c l s= - let xc=Constrextern.extern_constr false (Global.env ()) c in + let xc=Constrextern.extern_constr false (Global.env ()) Evd.empty c in str "| " ++ prlist Printer.pr_global l ++ str " : " ++ -- cgit v1.2.3