From 2d3916766d3f145643a994aa83174c98394d5baa Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 3 Mar 2015 21:45:42 +0100
Subject: Fix bug #3590, keeping evars that are not turned into named metas by
 pattern_of_constr in an evar_map, as they can appear in the context of said
 named metas, which is used by change. Not sure what to do in the PEvar case,
 which never matches anyway according to Constr_matching.matches.

---
 plugins/quote/quote.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 637e0e28d5..2a2ef30fb1 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -211,9 +211,9 @@ let compute_rhs bodyi index_of_f =
           let i = destRel (Array.last args) in
 	  PMeta (Some (coerce_meta_in i))
       | App (f,args) ->
-          PApp (snd (pattern_of_constr (Global.env()) Evd.empty f), Array.map aux args)
+          PApp (pi3 (pattern_of_constr (Global.env()) Evd.empty f), Array.map aux args)
       | Cast (c,_,_) -> aux c
-      | _ -> snd (pattern_of_constr (Global.env())(*FIXME*) Evd.empty c)
+      | _ -> pi3 (pattern_of_constr (Global.env())(*FIXME*) Evd.empty c)
   in
   aux bodyi
 
-- 
cgit v1.2.3


From 1b7e788a2bc6c7beb5d2e6971574e3349fd2a1cf Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 3 Mar 2015 23:20:53 +0100
Subject: Fix bug #3732: firstorder was using detyping to build existential
 instances and forgeting about the evars and universes that could appear
 there... dirty hack gone, using the evar map properly and avoiding needless
 constructions/deconstructions of terms.

---
 plugins/firstorder/instances.ml | 32 +++++++++++++-------------------
 1 file changed, 13 insertions(+), 19 deletions(-)

(limited to 'plugins')

diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index a88778c739..5912f0a0c3 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -113,24 +113,14 @@ let mk_open_instance id idc gl m t=
 	    Name id -> id
 	  | Anonymous ->  dummy_bvid in
   let revt=substl (List.init m (fun i->mkRel (m-i))) t in
-  let rec aux n avoid=
-    if Int.equal n 0 then [] else
+  let rec aux n avoid env evmap decls =
+    if Int.equal n 0 then evmap, decls else
       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 [] env evmap nt in
-  let rec raux n t=
-    if Int.equal n 0 then t else
-      match t with
-	  GLambda(loc,name,k,_,t0)->
-	    let t1=raux (n-1) t0 in
-	      GLambda(loc,name,k,GHole (Loc.ghost,Evar_kinds.BinderType name,Misctypes.IntroAnonymous,None),t1)
-	| _-> anomaly (Pp.str "can't happen") in
-  let ntt=try
-    fst (Pretyping.understand env evmap (raux m rawt))(*FIXME*)
-  with e when Errors.noncritical e ->
-    error "Untypable instance, maybe higher-order non-prenex quantification" in
-    decompose_lam_n_assum m ntt
+      let evmap, (c, _) = Evarutil.new_type_evar env evmap Evd.univ_flexible in
+      let decl = (Name nid,None,c) in
+	aux (n-1) (nid::avoid) (Environ.push_rel decl env) evmap (decl::decls) in
+  let evmap, decls = aux m [] env evmap [] in
+    evmap, decls, revt
 
 (* tactics   *)
 
@@ -159,11 +149,15 @@ let left_instance_tac (inst,id) continue seq=
 	    if m>0 then
 	      pf_constr_of_global id (fun idc ->
 		fun gl->
-		  let (rc,ot) = mk_open_instance id idc gl m t in
+		  let evmap,rc,ot = mk_open_instance id idc gl m t in
 		  let gt=
 		    it_mkLambda_or_LetIn
 		      (mkApp(idc,[|ot|])) rc in
-		    generalize [gt] gl)
+		  let evmap, _ =
+		    try Typing.e_type_of (pf_env gl) evmap gt
+		    with e when Errors.noncritical e ->
+		      error "Untypable instance, maybe higher-order non-prenex quantification" in
+		    tclTHEN (Refiner.tclEVARS evmap) (generalize [gt]) gl)
 	    else
 	      pf_constr_of_global id (fun idc ->
 		generalize [mkApp(idc,[|t|])])
-- 
cgit v1.2.3