- Remove create_evar_defs

- Be careful with consider_remaining_unif_problems: it might instantiate an evar, including the current goal!

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13995 85f007b7-540e-0410-9357-904b9bb8a0f7

12 files changed, 93 insertions, 82 deletions

diff --git a/dev/base_include b/dev/base_include
index 5d5e9e1dc..8e62140f3 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -38,7 +38,6 @@
 #install_printer  (* values *) ppvalues;;
 #install_printer  (* Idpred.t *) pp_idpred;;
 #install_printer  (* Cpred.t *) pp_cpred;;
-#install_printer  (* transparent_state *) pp_transparent_state;;
 #install_printer ppzipper;;
 #install_printer ppstack;;
 #install_printer ppatom;;
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 52765ff12..9a599c8ab 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1524,7 +1524,7 @@ let interp_open_constr sigma env c =
 
 let interp_open_constr_patvar sigma env c =
   let raw = intern_gen false sigma env c ~allow_patvar:true in
-  let sigma = ref (Evd.create_evar_defs sigma) in
+  let sigma = ref sigma in
   let evars = ref (Gmap.empty : (identifier,glob_constr) Gmap.t) in
   let rec patvar_to_evar r = match r with
     | GPatVar (loc,(_,id)) ->
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 8252ffb9e..c1c7f521a 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -547,4 +547,3 @@ let is_arity env c =
     let _ = dest_arity env c in
     true
   with NotArity -> false
-
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 525651493..bee8815a2 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -78,5 +78,5 @@ val dest_prod_assum : env -> types -> rel_context * types
 
 exception NotArity
 
-val dest_arity : env -> types -> arity (* raise NotArity if not an arity *)
+val dest_arity : env -> types -> arity (* raises NotArity if not an arity *)
 val is_arity   : env -> types -> bool
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index d2c05b913..17a1d3c34 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -1303,6 +1303,7 @@ let status_changed lev (pbty,_,t1,t2) =
 (* Rq: uncomplete algorithm if pbty = CONV_X_LEQ ! *)
 let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1),t2) =
   try
+    assert(Evd.is_undefined evd evk1);
     let t2 = whd_betaiota evd t2 in (* includes whd_evar *)
     let evd = match kind_of_term t2 with
       | Evar (evk2,args2 as ev2) ->
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 42dd243d0..4536cb570 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -691,17 +691,16 @@ module Pretyping_F (Coercion : Coercion.S) = struct
       | IsType ->
 	  (pretype_type empty_valcon env evdref lvar c).utj_val 
     in
-    if resolve_classes then (
-      evdref := Typeclasses.resolve_typeclasses ~onlyargs:false
-	~split:true ~fail:fail_evar env !evdref);
-    evdref := (try consider_remaining_unif_problems env !evdref
-	       with e when not resolve_classes -> 
-		 consider_remaining_unif_problems env 
-		   (Typeclasses.resolve_typeclasses ~onlyargs:false
-		      ~split:true ~fail:fail_evar env !evdref));
-    let c = if expand_evar then nf_evar !evdref c' else c' in
-      if fail_evar then check_evars env Evd.empty !evdref c;
-      c
+      if resolve_classes then
+	evdref := (Typeclasses.resolve_typeclasses ~onlyargs:false
+		   ~split:true ~fail:fail_evar env !evdref);
+      if fail_evar then
+	(* Resolve eagerly, potentially making wrong choices *)
+	evdref := (try consider_remaining_unif_problems env !evdref
+		   with e -> !evdref);
+      let c = if expand_evar then nf_evar !evdref c' else c' in
+	if fail_evar then check_evars env Evd.empty !evdref c;
+	c
 
   (* TODO: comment faire remonter l'information si le typage a resolu des
      variables du sigma original. il faudrait que la fonction de typage
@@ -709,7 +708,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
   *)
 
   let understand_judgment sigma env c =
-    let evdref = ref (create_evar_defs sigma) in
+    let evdref = ref sigma in
     let j = pretype empty_tycon env evdref ([],[]) c in
     let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~split:true
       ~fail:true env !evdref
@@ -729,7 +728,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
      extend env with some bindings *)
 
   let ise_pretype_gen expand_evar fail_evar resolve_classes sigma env lvar kind c =
-    let evdref = ref (Evd.create_evar_defs sigma) in
+    let evdref = ref sigma in
     let c = pretype_gen expand_evar fail_evar resolve_classes evdref env lvar kind c in
     !evdref, c
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 1bbecc4e2..828825aa0 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -341,7 +341,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
 		    match kind_of_term cN with App (f,l) -> (f,l) | _ -> (cN,[||]) in
 		    expand curenvnb pb b substn cM f1 l1 cN f2 l2
 
-  and reduce curenvnb pb b (sigma, _, _ as substn) cM cN =
+  and reduce curenvnb pb b (sigma, metas, evars as substn) cM cN =
     let cM' = do_reduce (fst curenvnb) sigma cM in
       if not (eq_constr cM cM') then
 	unirec_rec curenvnb pb true substn cM' cN
@@ -464,7 +464,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
       unirec_rec curenvnb pb b substn c1 (applist (c,(List.rev ks)))
 
   in
-  let evd = create_evar_defs sigma in
+  let evd = sigma in
     if (if occur_meta_or_undefined_evar evd m || occur_meta_or_undefined_evar evd n then false 
       else if (match flags.modulo_conv_on_closed_terms with
       | Some flags ->
@@ -487,64 +487,64 @@ let right = false
 let pop k = if k=0 then 0 else k-1
 
 let rec unify_with_eta keptside flags env sigma k1 k2 c1 c2 =
-  (* Reason up to limited eta-expansion: ci is allowed to start with ki lam *)
-  (* Question: try whd_betadeltaiota on ci if ki>0 ? *)
+(* Reason up to limited eta-expansion: ci is allowed to start with ki lam *)
+(* Question: try whd_betadeltaiota on ci if ki>0 ? *)
   match kind_of_term c1, kind_of_term c2 with
   | (Lambda (na,t1,c1'), Lambda (_,t2,c2')) ->
-      let env' = push_rel_assum (na,t1) env in
-      let sigma,metas,evars = unify_0 env sigma topconv flags t1 t2 in
-      let side,status,(sigma,metas',evars') =
-	unify_with_eta keptside flags env' sigma (pop k1) (pop k2) c1' c2'
-      in (side,status,(sigma,metas@metas',evars@evars'))
+    let env' = push_rel_assum (na,t1) env in
+    let sigma,metas,evars = unify_0 env sigma topconv flags t1 t2 in
+    let side,status,(sigma,metas',evars') =
+      unify_with_eta keptside flags env' sigma (pop k1) (pop k2) c1' c2'
+    in (side,status,(sigma,metas@metas',evars@evars'))
   | (Lambda (na,t,c1'),_) when k2 > 0 ->
-      let env' = push_rel_assum (na,t) env in
-      let side = left in (* expansion on the right: we keep the left side *)
+    let env' = push_rel_assum (na,t) env in
+    let side = left in (* expansion on the right: we keep the left side *)
       unify_with_eta side flags env' sigma (pop k1) (k2-1)
-	c1' (mkApp (lift 1 c2,[|mkRel 1|]))
+      c1' (mkApp (lift 1 c2,[|mkRel 1|]))
   | (_,Lambda (na,t,c2')) when k1 > 0 ->
-      let env' = push_rel_assum (na,t) env in
-      let side = right in (* expansion on the left: we keep the right side *)
+    let env' = push_rel_assum (na,t) env in
+    let side = right in (* expansion on the left: we keep the right side *)
       unify_with_eta side flags env' sigma (k1-1) (pop k2)
-	(mkApp (lift 1 c1,[|mkRel 1|])) c2'
+      (mkApp (lift 1 c1,[|mkRel 1|])) c2'
   | _ ->
-      (keptside,ConvUpToEta(min k1 k2),
-       unify_0 env sigma topconv flags c1 c2)
-
+    (keptside,ConvUpToEta(min k1 k2),
+     unify_0 env sigma topconv flags c1 c2)
+    
 (* We solved problems [?n =_pb u] (i.e. [u =_(opp pb) ?n]) and [?n =_pb' u'],
    we now compute the problem on [u =? u'] and decide which of u or u' is kept
 
    Rem: the upper constraint is lost in case u <= ?n <= u' (and symmetrically
    in the case u' <= ?n <= u)
  *)
-
+    
 let merge_instances env sigma flags st1 st2 c1 c2 =
   match (opp_status st1, st2) with
   | (UserGiven, ConvUpToEta n2) ->
-      unify_with_eta left flags env sigma 0 n2 c1 c2
+    unify_with_eta left flags env sigma 0 n2 c1 c2
   | (ConvUpToEta n1, UserGiven) ->
-      unify_with_eta right flags env sigma n1 0 c1 c2
+    unify_with_eta right flags env sigma n1 0 c1 c2
   | (ConvUpToEta n1, ConvUpToEta n2) ->
-      let side = left (* arbitrary choice, but agrees with compatibility *) in
+    let side = left (* arbitrary choice, but agrees with compatibility *) in
       unify_with_eta side flags env sigma n1 n2 c1 c2
   | ((IsSubType | ConvUpToEta _ | UserGiven as oppst1),
      (IsSubType | ConvUpToEta _ | UserGiven)) ->
-      let res = unify_0 env sigma Cumul flags c2 c1 in
+    let res = unify_0 env sigma Cumul flags c2 c1 in
       if oppst1=st2 then (* arbitrary choice *) (left, st1, res)
       else if st2=IsSubType or st1=UserGiven then (left, st1, res)
       else (right, st2, res)
   | ((IsSuperType | ConvUpToEta _ | UserGiven as oppst1),
      (IsSuperType | ConvUpToEta _ | UserGiven)) ->
-      let res = unify_0 env sigma Cumul flags c1 c2 in
+    let res = unify_0 env sigma Cumul flags c1 c2 in
       if oppst1=st2 then (* arbitrary choice *) (left, st1, res)
       else if st2=IsSuperType or st1=UserGiven then (left, st1, res)
       else (right, st2, res)
   | (IsSuperType,IsSubType) ->
-      (try (left, IsSubType, unify_0 env sigma Cumul flags c2 c1)
-       with _ -> (right, IsSubType, unify_0 env sigma Cumul flags c1 c2))
+    (try (left, IsSubType, unify_0 env sigma Cumul flags c2 c1)
+     with _ -> (right, IsSubType, unify_0 env sigma Cumul flags c1 c2))
   | (IsSubType,IsSuperType) ->
-      (try (left, IsSuperType, unify_0 env sigma Cumul flags c1 c2)
-       with _ -> (right, IsSuperType, unify_0 env sigma Cumul flags c2 c1))
-
+    (try (left, IsSuperType, unify_0 env sigma Cumul flags c1 c2)
+     with _ -> (right, IsSuperType, unify_0 env sigma Cumul flags c2 c1))
+    
 (* Unification
  *
  * Procedure:
@@ -600,14 +600,14 @@ let applyHead env evd n c  =
       (evd, c)
     else
       match kind_of_term (whd_betadeltaiota env evd cty) with
-        | Prod (_,c1,c2) ->
-            let (evd',evar) =
-	      Evarutil.new_evar evd env ~src:(dummy_loc,GoalEvar) c1 in
-	    apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd'
-	| _ -> error "Apply_Head_Then"
+      | Prod (_,c1,c2) ->
+        let (evd',evar) =
+	  Evarutil.new_evar evd env ~src:(dummy_loc,GoalEvar) c1 in
+	  apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd'
+      | _ -> error "Apply_Head_Then"
   in
-  apprec n c (Typing.type_of env evd c) evd
-
+    apprec n c (Typing.type_of env evd c) evd
+    
 let is_mimick_head ts f =
   match kind_of_term f with
   | Const c -> not (Closure.is_transparent_constant ts c)
@@ -625,14 +625,14 @@ let try_to_coerce env evd c cty tycon =
 let w_coerce_to_type env evd c cty mvty =
   let evd,mvty = pose_all_metas_as_evars env evd mvty in
   let tycon = mk_tycon_type mvty in
-  try try_to_coerce env evd c cty tycon
-  with e when precatchable_exception e ->
+    try try_to_coerce env evd c cty tycon
+    with e when precatchable_exception e ->
     (* inh_conv_coerce_rigid_to should have reasoned modulo reduction
        but there are cases where it though it was not rigid (like in
        fst (nat,nat)) and stops while it could have seen that it is rigid *)
     let cty = Tacred.hnf_constr env evd cty in
-    try_to_coerce env evd c cty tycon
-
+      try_to_coerce env evd c cty tycon
+	  
 let w_coerce env evd mv c =
   let cty = get_type_of env evd c in
   let mvty = Typing.meta_type evd mv in
@@ -693,6 +693,7 @@ let w_merge env with_types flags (evd,metas,evars) =
 	    unify_0 curenv evd topconv flags rhs v in
 	  w_merge_rec evd (metas'@metas) (evars''@evars') eqns
     	else begin
+	  (* This can make rhs' ill-typed if metas are *)
           let rhs' = subst_meta_instances metas rhs in
           match kind_of_term rhs with
 	  | App (f,cl) when occur_meta rhs' ->
@@ -708,9 +709,9 @@ let w_merge env with_types flags (evd,metas,evars) =
 		  metas evars' eqns
 
           | _ ->
-	    let evd', rhs'' = pose_all_metas_as_evars curenv evd rhs' in
-	      w_merge_rec (solve_simple_evar_eqn flags.modulo_delta_types curenv evd' ev rhs'')
-		metas evars' eqns
+	      let evd', rhs'' = pose_all_metas_as_evars curenv evd rhs' in
+		w_merge_rec (solve_simple_evar_eqn flags.modulo_delta_types curenv evd' ev rhs'')
+		  metas evars' eqns
 	end
     | [] ->
 
@@ -726,7 +727,8 @@ let w_merge env with_types flags (evd,metas,evars) =
               (* No coercion needed: delay the unification of types *)
 	      ((evd,c),([],[])),(mv,status,c)::eqns
 	  else
-	    ((evd,c),([],[])),eqns in
+	    ((evd,c),([],[])),eqns 
+	in
 	  if meta_defined evd mv then
 	    let {rebus=c'},(status',_) = meta_fvalue evd mv in
             let (take_left,st,(evd,metas',evars')) =
@@ -739,23 +741,30 @@ let w_merge env with_types flags (evd,metas,evars) =
               w_merge_rec evd' (metas'@metas@metas'') (evars'@evars'') eqns
     	  else
 	    let evd' = meta_assign mv (c,(status,TypeProcessed)) evd in
-	      w_merge_rec evd' (metas@metas'') evars'' eqns
+	      w_merge_rec evd' (metas''@metas) evars'' eqns
     | [] ->
-
-    (* Process type eqns *)
-    match eqns with
-    | (mv,status,c)::eqns ->
-        let (evd,metas,evars) = unify_type env evd flags mv status c in
-        w_merge_rec evd metas evars eqns
-    | [] -> evd
-
+	(* Process type eqns *)
+	let rec process_eqns failures = function
+	  | (mv,status,c)::eqns ->
+              (match (try Inl (unify_type env evd flags mv status c)
+		      with e -> Inr e)
+	       with 
+	       | Inr e -> process_eqns (((mv,status,c),e)::failures) eqns
+	       | Inl (evd,metas,evars) ->
+		   w_merge_rec evd metas evars (List.map fst failures @ eqns))
+	  | [] -> 
+	      (match failures with
+	       | [] -> evd
+	       | ((mv,status,c),e)::_ -> raise e)
+	in process_eqns [] eqns
+	      
   and mimick_undefined_evar evd flags hdc nargs sp =
     let ev = Evd.find_undefined evd sp in
     let sp_env = Global.env_of_context ev.evar_hyps in
     let (evd', c) = applyHead sp_env evd nargs hdc in
     let (evd'',mc,ec) =
       unify_0 sp_env evd' Cumul flags
-        (Retyping.get_type_of sp_env evd' c) ev.evar_concl in
+        (get_type_of sp_env evd' c) ev.evar_concl in
     let evd''' = w_merge_rec evd'' mc ec [] in
     if evd' == evd'''
     then Evd.define sp c evd'''
@@ -782,13 +791,13 @@ let check_types env flags (sigma,_,_ as subst) m n =
   if isEvar_or_Meta (fst (whd_stack sigma m)) then
     unify_0_with_initial_metas subst true env Cumul
       flags
-      (Retyping.get_type_of env sigma n)
-      (Retyping.get_type_of env sigma m)
+      (get_type_of env sigma n)
+      (get_type_of env sigma m)
   else if isEvar_or_Meta (fst (whd_stack sigma n)) then
     unify_0_with_initial_metas subst true env Cumul
       flags
-      (Retyping.get_type_of env sigma m)
-      (Retyping.get_type_of env sigma n)
+      (get_type_of env sigma m)
+      (get_type_of env sigma n)
   else subst
 
 let w_unify_core_0 env with_types cv_pb flags m n evd =
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 4dfe03500..64c5c5a9e 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -171,7 +171,10 @@ and e_my_find_search db_list local_db hdc concl =
               tclTHEN (with_prods nprods (term,cl) (unify_e_resolve flags))
 		(e_trivial_fail_db db_list local_db)
 	  | Unfold_nth c -> tclWEAK_PROGRESS (unfold_in_concl [all_occurrences,c])
-	  | Extern tacast -> conclPattern concl p tacast
+	  | Extern tacast -> 
+	    tclTHEN
+	      (fun gl -> Refiner.tclEVARS (mark_unresolvables (project gl)) gl)
+	      (conclPattern concl p tacast)
       in
 	match t with
 	| Extern _ -> (tac,b,true,lazy (pr_autotactic t))
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 4d8fc0e44..a01799b18 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -1074,7 +1074,7 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul
       | None -> (sort, inverse sort impl)
       | Some _ -> (sort, impl)
   in
-  let evars = (create_evar_defs sigma, Evd.empty) in
+  let evars = (sigma, Evd.empty) in
   let eq = apply_strategy strat env avoid concl (Some cstr) evars in
     match eq with
     | Some (Some (p, evars, car, oldt, newt)) ->
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 735de9371..b33942b0c 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1253,7 +1253,8 @@ let solvable_by_tactic env evi (ev,args) src =
 
 let solve_remaining_evars fail_evar use_classes env initial_sigma evd c =
   let evdref =
-    if use_classes then ref (Typeclasses.resolve_typeclasses ~fail:true env evd)
+    if use_classes then 
+      ref (Typeclasses.resolve_typeclasses ~split:true ~fail:fail_evar env evd)
     else ref evd in
   let rec proc_rec c =
     let c = Reductionops.whd_evar !evdref c in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 4e6a293c9..d96090833 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -590,7 +590,7 @@ let resolve_classes gl =
   let env = pf_env gl and evd = project gl in
     if Evd.is_empty evd then tclIDTAC gl
     else
-      let evd' = Typeclasses.resolve_typeclasses env (Evd.create_evar_defs evd) in
+      let evd' = Typeclasses.resolve_typeclasses env evd in
 	(tclTHEN (tclEVARS evd') tclNORMEVAR) gl
 
 (**************************)
@@ -2391,7 +2391,7 @@ let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id gl =
 let specialize_eqs id gl =
   let env = pf_env gl in
   let ty = pf_get_hyp_typ gl id in
-  let evars = ref (create_evar_defs (project gl)) in
+  let evars = ref (project gl) in
   let unif env evars c1 c2 = Evarconv.e_conv env evars c2 c1 in
   let rec aux in_eqs ctx acc ty =
     match kind_of_term ty with
@@ -3440,6 +3440,6 @@ let unify ?(state=full_transparent_state) x y gl =
 	modulo_conv_on_closed_terms = Some state}
     in
     let evd = w_unify false (pf_env gl) Reduction.CONV
-      ~flags x y (Evd.create_evar_defs (project gl))
+      ~flags x y (project gl)
     in tclEVARS evd gl
   with _ -> tclFAIL 0 (str"Not unifiable") gl
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index 7e806cf10..a72a6b5ab 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -311,7 +311,7 @@ let start_proof_with_initialization kind recguard thms snl hook =
       start_proof id kind t ?init_tac hook ~compute_guard:guard
 
 let start_proof_com kind thms hook =
-  let evdref = ref (create_evar_defs Evd.empty) in
+  let evdref = ref Evd.empty in
   let env0 = Global.env () in
   let thms = List.map (fun (sopt,(bl,t,guard)) ->
     let impls, ((env, ctx), imps) = interp_context_evars evdref env0 bl in