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/instances.ml | 2 +-
 plugins/firstorder/sequent.ml   | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/firstorder')

diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 076107450b..6fd934654d 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -118,7 +118,7 @@ let mk_open_instance id idc gl m t=
       let nid=(fresh_id avoid var_id gl) in
 	(Name nid,None,dummy_constr)::(aux (n-1) (nid::avoid)) in
   let nt=it_mkLambda_or_LetIn revt (aux m []) in
-  let rawt=Detyping.detype false [] [] nt in
+  let rawt=Detyping.detype false [] [] evmap nt in
   let rec raux n t=
     if Int.equal n 0 then t else
       match t with
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 43bb6dbbf8..afa178832f 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