Fixes to make Ynot compile with the trunk:

- Choose one of the possible instances of an evar when considering
remaining unification constraints: otherwise we just do nothing and
some evars remain uninstantiated.
- Normalise the goal w.r.t. evars before subst, to avoid a double vision 
problem: the substituted variable appears only in an instance of an evar
and when we try the rewrite it has been substituted making the dependency
disappear.
- Hack to correcly handle let-in annotations which are internalized as 
casts: they're really typing constraints. Shouldn't we just change the 
AST to have the type at rawconstr let-in nodes?


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

5 files changed, 40 insertions, 30 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index d185bd64e..bb28a09bc 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -505,7 +505,7 @@ let first_order_unification env evd (ev1,l1) (term2,l2) =
       if is_defined_evar i ev1 then
 	evar_conv_x env i CONV t2 (mkEvar ev1)
       else
-	solve_simple_eqn evar_conv_x env i (CONV,ev1,t2))]
+	solve_simple_eqn ~choose:true evar_conv_x env i (CONV,ev1,t2))]
 
 let choose_less_dependent_instance evk evd term args =
   let evi = Evd.find ( evd) evk in
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 29b5b87a7..6c8d4e3de 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -839,7 +839,7 @@ let expand_rhs env sigma subst rhs =
 exception NotInvertibleUsingOurAlgorithm of constr
 exception NotEnoughInformationToProgress
 
-let rec invert_definition env evd (evk,argsv as ev) rhs =
+let rec invert_definition choose env evd (evk,argsv as ev) rhs =
   let evdref = ref evd in
   let progress = ref false in
   let evi = Evd.find ( evd) evk in
@@ -850,7 +850,11 @@ let rec invert_definition env evd (evk,argsv as ev) rhs =
     (* Evar/Var problem: unifiable iff variable projectable from ev subst *)
     try 
       let sols = find_projectable_vars true env ( !evdref) t subst in
-      let c, p = filter_solution sols in
+      let c, p = match sols with
+	| [] -> raise Not_found
+	| [id,p] -> (mkVar id, p)
+	| (id,p)::_::_ -> if choose then (mkVar id, p) else raise NotUnique
+      in
       let ty = lazy (Retyping.get_type_of env ( !evdref) t) in
       let evd = do_projection_effects evar_define env ty !evdref p in
       evdref := evd;
@@ -926,9 +930,9 @@ and occur_existential evm c =
     | _ -> iter_constr occrec c
   in try occrec c; false with Occur -> true
 
-and evar_define env (evk,_ as ev) rhs evd =
+and evar_define ?(choose=false) env (evk,_ as ev) rhs evd =
   try
-    let (evd',body) = invert_definition env evd ev rhs in
+    let (evd',body) = invert_definition choose env evd ev rhs in
     if occur_meta body then error "Meta cannot occur in evar body.";
     (* invert_definition may have instantiate some evars of rhs with evk *)
     (* so we recheck acyclicity *)
@@ -1123,7 +1127,7 @@ let solve_refl conv_algo env evd evk argsv1 argsv2 =
  * if the problem couldn't be solved. *)
 
 (* Rq: uncomplete algorithm if pbty = CONV_X_LEQ ! *)
-let solve_simple_eqn conv_algo env evd (pbty,(evk1,args1 as ev1),t2) =
+let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1),t2) =
   try
     let t2 = whd_evar ( evd) t2 in
     let evd = match kind_of_term t2 with
@@ -1135,15 +1139,17 @@ let solve_simple_eqn conv_algo env evd (pbty,(evk1,args1 as ev1),t2) =
 	    then solve_evar_evar evar_define env evd ev1 ev2
 	    else add_conv_pb (pbty,env,mkEvar ev1,t2) evd
       | _ ->
-	  let evd = evar_define env ev1 t2 evd in
-	  let evm =  evd in
-	  let evi = Evd.find evm evk1 in
-	    if occur_existential evm evi.evar_concl then
+	  let evd = evar_define ~choose env ev1 t2 evd in
+	  let evi = Evd.find evd evk1 in
+	    if occur_existential evd evi.evar_concl then
 	      let evenv = evar_env evi in
 	      let evc = nf_isevar evd evi.evar_concl in
-	      let body = match evi.evar_body with Evar_defined b -> b | Evar_empty -> assert false in
-	      let ty = nf_isevar evd (Retyping.get_type_of_with_meta evenv evm (metas_of evd) body) in
-		add_conv_pb (Reduction.CUMUL,evenv,ty,evc) evd
+		match evi.evar_body with 
+		| Evar_defined body -> 
+		    let ty = nf_isevar evd (Retyping.get_type_of_with_meta evenv evd (metas_of evd) body) in
+		      add_conv_pb (Reduction.CUMUL,evenv,ty,evc) evd
+		| Evar_empty -> (* Resulted in a constraint *) 
+		    evd
 	    else evd
     in
     let (evd,pbs) = extract_changed_conv_pbs evd status_changed in
@@ -1238,7 +1244,7 @@ let mk_valcon c = Some c
    cumulativity now includes Prop and Set in Type...
    It is, but that's not too bad *)
 let define_evar_as_abstraction abs evd (ev,args) =
-  let evi = Evd.find ( evd) ev in
+  let evi = Evd.find evd ev in
   let evenv = evar_unfiltered_env evi in
   let (evd1,dom) = new_evar evd evenv (new_Type()) ~filter:(evar_filter evi) in
   let nvar =
@@ -1254,8 +1260,8 @@ let define_evar_as_abstraction abs evd (ev,args) =
   let evrng =
     fst (destEvar rng), array_cons (mkRel 1) (Array.map (lift 1) args) in
   let prod' = abs (Name nvar, mkEvar evdom, mkEvar evrng) in
-  (evd3,prod')
-
+    (evd3,prod')
+      
 let define_evar_as_product evd (ev,args) =
   define_evar_as_abstraction (fun t -> mkProd t) evd (ev,args)
 
@@ -1266,7 +1272,6 @@ let define_evar_as_sort evd (ev,args) =
   let s = new_Type () in
   Evd.define ev s evd, destSort s
 
-
 (* We don't try to guess in which sort the type should be defined, since
    any type has type Type. May cause some trouble, but not so far... *)
 
@@ -1278,27 +1283,26 @@ let judge_of_new_Type () = Typeops.judge_of_type (new_univ ())
    an evar instantiate it with the product of 2 new evars. *)
 
 let split_tycon loc env evd tycon = 
-  let rec real_split c = 
-    let sigma =  evd in
-    let t = whd_betadeltaiota env sigma c in
+  let rec real_split evd c = 
+    let t = whd_betadeltaiota env evd c in
       match kind_of_term t with
 	| Prod (na,dom,rng) -> evd, (na, dom, rng)
 	| Evar ev when not (Evd.is_defined_evar evd ev) ->
 	    let (evd',prod) = define_evar_as_product evd ev in
 	    let (_,dom,rng) = destProd prod in
 	      evd',(Anonymous, dom, rng)
-	| _ -> error_not_product_loc loc env sigma c
+	| _ -> error_not_product_loc loc env evd c
   in
     match tycon with
       | None -> evd,(Anonymous,None,None)
       | Some (abs, c) ->
 	  (match abs with
 	       None -> 
-		 let evd', (n, dom, rng) = real_split c in
+		 let evd', (n, dom, rng) = real_split evd c in
 		   evd', (n, mk_tycon dom, mk_tycon rng)
 	     | Some (init, cur) ->
 		 if cur = 0 then 
-		   let evd', (x, dom, rng) = real_split c in
+		   let evd', (x, dom, rng) = real_split evd c in
 		     evd, (Anonymous, 
 			  Some (None, dom), 
 			  Some (None, rng))
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 9190d8a97..d35616ae2 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -53,11 +53,11 @@ val make_pure_subst : evar_info -> constr array -> (identifier * constr) list
 (***********************************************************)
 (* Instantiate evars *)
 
-(* [evar_define env ev c] try to instantiate [ev] with [c] (typed in [env]),
+(* [evar_define choose env ev c] try to instantiate [ev] with [c] (typed in [env]),
    possibly solving related unification problems, possibly leaving open
-   some problems that cannot be solved in a unique way;
-   failed if the instance is not valid for the given [ev] *)
-val evar_define : env -> existential -> constr -> evar_defs -> evar_defs
+   some problems that cannot be solved in a unique way (except if choose is
+   true); fails if the instance is not valid for the given [ev] *)
+val evar_define : ?choose:bool -> env -> existential -> constr -> evar_defs -> evar_defs
 
 (***********************************************************)
 (* Evars/Metas switching... *)
@@ -80,7 +80,7 @@ val solve_refl :
     evar_defs
 val solve_simple_eqn :
   (env ->  evar_defs -> conv_pb -> constr -> constr -> evar_defs * bool)
-  -> env ->  evar_defs -> conv_pb * existential * constr ->
+  -> ?choose:bool -> env ->  evar_defs -> conv_pb * existential * constr ->
     evar_defs * bool
 
 (* [check_evars env initial_sigma extended_sigma c] fails if some
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 0fd2fccb4..562e6ec93 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -443,7 +443,13 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	  inh_conv_coerce_to_tycon loc env evdref resj tycon
 	    
     | RLetIn(loc,name,c1,c2)      ->
-	let j = pretype empty_tycon env evdref lvar c1 in
+	let j = 
+	  match c1 with
+	  | RCast (loc, c, CastConv (DEFAULTcast, t)) ->
+	      let tj = pretype_type empty_valcon env evdref lvar t in		
+		pretype (mk_tycon tj.utj_val) env evdref lvar c
+	  | _ -> pretype empty_tycon env evdref lvar c1
+	in
 	let t = refresh_universes j.uj_type in
 	let var = (name,Some j.uj_val,t) in
         let tycon = lift_tycon 1 tycon in
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 3af4fa171..99767afc0 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1216,7 +1216,7 @@ let subst_one x gl =
        tclMAP introtac depdecls]) @
      [tclTRY (clear [x;hyp])]) gl
 
-let subst = tclMAP subst_one
+let subst ids = tclTHEN tclNORMEVAR (tclMAP subst_one ids)
 
 let subst_all gl =
   let test (_,c) =