From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 27 Dec 2016 16:53:30 +0100
Subject: Imported Upstream version 8.6

---
 proofs/clenv.ml | 69 +++++++++++++++++++++++++++++++++++++++++++--------------
 1 file changed, 52 insertions(+), 17 deletions(-)

(limited to 'proofs/clenv.ml')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 88e1bce9..0a90e0db 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Names
 open Nameops
@@ -24,6 +24,7 @@ open Pretype_errors
 open Evarutil
 open Unification
 open Misctypes
+open Sigma.Notations
 
 (* Abbreviations *)
 
@@ -71,7 +72,7 @@ let clenv_get_type_of ce c = Retyping.get_type_of (cl_env ce) (cl_sigma ce) c
 exception NotExtensibleClause
 
 let clenv_push_prod cl =
-  let typ = whd_betadeltaiota (cl_env cl) (cl_sigma cl) (clenv_type cl) in
+  let typ = whd_all (cl_env cl) (cl_sigma cl) (clenv_type cl) in
   let rec clrec typ = match kind_of_term typ with
     | Cast (t,_,_) -> clrec t
     | Prod (na,t,u) ->
@@ -108,7 +109,7 @@ let clenv_environments evd bound t =
       | (n, Cast (t,_,_)) -> clrec (e,metas) n t
       | (n, Prod (na,t1,t2)) ->
 	  let mv = new_meta () in
-	  let dep = dependent (mkRel 1) t2 in
+	  let dep = not (noccurn 1 t2) in
 	  let na' = if dep then na else Anonymous in
 	  let e' = meta_declare mv t1 ~name:na' e in
 	  clrec (e', (mkMeta mv)::metas) (Option.map ((+) (-1)) n)
@@ -119,7 +120,7 @@ let clenv_environments evd bound t =
   clrec (evd,[]) bound t
 
 let mk_clenv_from_env env sigma n (c,cty) =
-  let evd = create_goal_evar_defs sigma in
+  let evd = clear_metas sigma in
   let (evd,args,concl) = clenv_environments evd n cty in
   { templval = mk_freelisted (applist (c,args));
     templtyp = mk_freelisted concl;
@@ -335,22 +336,15 @@ let clenv_pose_metas_as_evars clenv dep_mvs =
       else
         let src = evar_source_of_meta mv clenv.evd in
         let src = adjust_meta_source clenv.evd mv src in
-	let (evd,evar) = new_evar (cl_env clenv) clenv.evd ~src ty in
+        let evd = Sigma.Unsafe.of_evar_map clenv.evd in
+	let Sigma (evar, evd, _) = new_evar (cl_env clenv) evd ~src ty in
+	let evd = Sigma.to_evar_map evd in
 	let clenv = clenv_assign mv evar {clenv with evd=evd} in
 	fold clenv mvs in
   fold clenv dep_mvs
 
 (******************************************************************)
 
-let connect_clenv gls clenv =
-  let evd = evars_reset_evd ~with_conv_pbs:true gls.sigma clenv.evd in
-  { clenv with
-    evd = evd ;
-    env = Goal.V82.env evd (sig_it gls) }
-
-(* let connect_clenv_key = Profile.declare_profile "connect_clenv";; *)
-(* let connect_clenv = Profile.profile2 connect_clenv_key connect_clenv *)
-
 (* [clenv_fchain mv clenv clenv']
  *
  * Resolves the value of "mv" (which must be undefined) in clenv to be
@@ -432,6 +426,44 @@ let check_bindings bl =
 	   str " occurs more than once in binding list.")
     | [] -> ()
 
+let explain_no_such_bound_variable evd id =
+  let fold l (n, clb) =
+    let na = match clb with
+    | Cltyp (na, _) -> na
+    | Clval (na, _, _) -> na
+    in
+    if na != Anonymous then out_name na :: l else l
+  in
+  let mvl = List.fold_left fold [] (Evd.meta_list evd) in
+  errorlabstrm "Evd.meta_with_name"
+    (str"No such bound variable " ++ pr_id id ++
+     (if mvl == [] then str " (no bound variables at all in the expression)."
+      else
+        (str" (possible name" ++
+         str (if List.length mvl == 1 then " is: " else "s are: ") ++
+         pr_enum pr_id mvl ++ str").")))
+
+let meta_with_name evd id =
+  let na = Name id in
+  let fold (l1, l2 as l) (n, clb) =
+    let (na',def) = match clb with
+    | Cltyp (na, _) -> (na, false)
+    | Clval (na, _, _) -> (na, true)
+    in
+    if Name.equal na na' then if def then (n::l1,l2) else (n::l1,n::l2)
+    else l
+  in
+  let (mvl, mvnodef) = List.fold_left fold ([], []) (Evd.meta_list evd) in
+  match mvnodef, mvl with
+    | _,[]  ->
+      explain_no_such_bound_variable evd id
+    | ([n],_|_,[n]) ->
+        n
+    | _  ->
+        errorlabstrm "Evd.meta_with_name"
+          (str "Binder name \"" ++ pr_id id ++
+           strbrk "\" occurs more than once in clause.")
+
 let meta_of_binder clause loc mvs = function
   | NamedHyp s -> meta_with_name clause.evd s
   | AnonHyp n ->
@@ -459,7 +491,8 @@ let clenv_unify_binding_type clenv c t u =
       let evd,c = w_coerce_to_type (cl_env clenv) clenv.evd c t u in
       TypeProcessed, { clenv with evd = evd }, c
     with 
-      | PretypeError (_,_,ActualTypeNotCoercible (_,_,NotClean _)) as e ->
+      | PretypeError (_,_,ActualTypeNotCoercible (_,_,
+          (NotClean _ | ConversionFailed _))) as e ->
 	  raise e
       | e when precatchable_exception e ->
 	  TypeNotProcessed, clenv, c
@@ -576,7 +609,9 @@ let make_evar_clause env sigma ?len t =
     | Cast (t, _, _) -> clrec (sigma, holes) n t
     | Prod (na, t1, t2) ->
       let store = Typeclasses.set_resolvable Evd.Store.empty false in
-      let sigma, ev = new_evar ~store env sigma t1 in
+      let sigma = Sigma.Unsafe.of_evar_map sigma in
+      let Sigma (ev, sigma, _) = new_evar ~store env sigma t1 in
+      let sigma = Sigma.to_evar_map sigma in
       let dep = dependent (mkRel 1) t2 in
       let hole = {
         hole_evar = ev;
@@ -628,7 +663,7 @@ let evar_of_binder holes = function
   try
     let h = List.nth holes (pred n) in
     h.hole_evar
-  with e when Errors.noncritical e ->
+  with e when CErrors.noncritical e ->
     errorlabstrm "" (str "No such binder.")
 
 let define_with_type sigma env ev c =
-- 
cgit v1.2.3