Various improvements in handling of evars in general and typing

constraints in Program:
- normalize types and defs of local fixpoints before checking the
guardness condition to avoid having to give type annotations, e.g:
<<
Definition fold (A B : Set) (f : B -> A -> B) : B -> tree A -> B :=
  fix aux acc t :=
    match t with
      | Leaf x => f acc x
      | Node l => fold_left aux l acc
    end.
>>
- add new inh_coerce_to_prod to allow coercion of the typing constraint
to a product before trying to split it. It's a noop in standard mode, 
and forgets subsets in Program. Allows to typecheck:
<< (λ x, x) : { f : nat -> nat | ... } >>.
- Better handling of the "abstract" typing constraints in Program.
- Correctly normalize w.r.t. evars. the tycon given by users in Program.


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

9 files changed, 78 insertions, 83 deletions

diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index 11a7f1941a..9c559e6cba 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -111,21 +111,10 @@ module Coercion = struct
       : (Term.constr -> Term.constr) option 
       =
     let x = nf_evar (evars_of !isevars) x and y = nf_evar (evars_of !isevars) y in
-(*       (try debug 1 (str "Coerce called for " ++ (my_print_constr env x) ++  *)
-(* 		  str " and "++ my_print_constr env y ++  *)
-(* 		  str " with evars: " ++ spc () ++ *)
-(* 		  my_print_evardefs !isevars); *)
-(*        with _ -> ()); *)
     let rec coerce_unify env x y =
-(*       (try debug 1 (str "coerce_unify from " ++ (my_print_constr env x) ++  *)
-(* 		  str " to "++ my_print_constr env y) *)
-(*        with _ -> ()); *)
       let x = hnf env isevars x and y = hnf env isevars y in
 	try 
 	  isevars := the_conv_x_leq env x y !isevars;
-	  (* 	(try debug 1 (str "Unified " ++ (my_print_constr env x) ++  *)
-	  (* 			str " and "++ my_print_constr env y); *)
-	  (* 	 with _ -> ()); *)
 	  None
 	with Reduction.NotConvertible -> coerce' env x y
     and coerce' env x y : (Term.constr -> Term.constr) option =
@@ -133,10 +122,6 @@ module Coercion = struct
       let rec coerce_application typ typ' c c' l l' =
 	let len = Array.length l in
 	let rec aux tele typ typ' i co = 
-(* 	  (try trace (str "coerce_application.aux from " ++ (my_print_constr env x) ++ *)
-(* 			 str " to "++ my_print_constr env y *)
-(* 		       ++ str "in env:" ++ my_print_env env); *)
-(* 	    with _ -> ()); *)
 	  if i < len then
 	    let hdx = l.(i) and hdy = l'.(i) in
 	      try isevars := the_conv_x_leq env hdx hdy !isevars;
@@ -165,10 +150,6 @@ module Coercion = struct
 	  else Some co
 	in aux [] typ typ' 0 (fun x -> x)
       in
-(* 	(try trace (str "coerce' from " ++ (my_print_constr env x) ++ *)
-(* 		       str " to "++ my_print_constr env y *)
-(* 		       ++ str "in env:" ++ my_print_env env); *)
-(* 	  with _ -> ()); *)
 	match (kind_of_term x, kind_of_term y) with
 	  | Sort s, Sort s' -> 
 	      (match s, s' with
@@ -179,13 +160,6 @@ module Coercion = struct
 	  | Prod (name, a, b), Prod (name', a', b') ->
 	      let name' = Name (Nameops.next_ident_away (id_of_string "x") (Termops.ids_of_context env)) in
 	      let env' = push_rel (name', None, a') env in
-		
-(* 	      let c1 = coerce_unify env' (lift 1 a') (lift 1 a) in *)
-(* 	      let name'' = Name (Nameops.next_ident_away (id_of_string "x'") (Termops.ids_of_context env)) in *)
-(* 	      let env'' = push_rel (name'', Some (app_opt c1 (mkRel 1)), lift 1 a) env' in *)
-(* 	      let c2 = coerce_unify env'' (liftn 1 1 b) (lift 1 b') in *)
-(* 				     mkLetIn (name'', app_opt c1 (mkRel 1), (lift 1 a), *)
-
 	      let c1 = coerce_unify env' (lift 1 a') (lift 1 a) in
 		(* env, x : a' |- c1 : lift 1 a' > lift 1 a *)
 	      let coec1 = app_opt c1 (mkRel 1) in
@@ -295,7 +269,6 @@ module Coercion = struct
     and subset_coerce env isevars x y =
       match disc_subset x with
 	  Some (u, p) -> 
-	    (* trace (str "Inserting projection ");	     *)
 	    let c = coerce_unify env u y in
 	    let f x = 
 	      app_opt c (mkApp ((Lazy.force sig_).proj1, 
@@ -423,7 +396,11 @@ module Coercion = struct
       isevars, { uj_val = app_opt ct j.uj_val; 
 		 uj_type = typ' }
 
-
+  let inh_coerce_to_prod loc env isevars t =
+    let typ = whd_betadeltaiota env (evars_of isevars) (snd t) in
+    let _, typ' = mu env isevars typ in
+      isevars, (fst t, typ')
+	
   let inh_coerce_to_fail env evd rigidonly v t c1 =
     if rigidonly & not (Heads.is_rigid env c1 && Heads.is_rigid env t)
     then
@@ -508,8 +485,7 @@ module Coercion = struct
       try let rels, rng = decompose_prod_n nabs t in
 	(* The final range free variables must have been replaced by evars, we accept only that evars
 	   in rng are applied to free vars. *)
-	if noccur_with_meta 0 (succ nabsinit) rng then (
-(* 	  trace (str "No occur between 0 and " ++ int (succ nabsinit)); *)
+	if noccur_with_meta 0 (succ nabs) rng then (
 	  let env', t, t' =
 	    let env' = List.fold_right (fun (n, t) env -> push_rel (n, None, t) env) rels env in
 	      env', rng, lift nabs t'
@@ -523,6 +499,4 @@ module Coercion = struct
 		error_cannot_coerce env' sigma (t, t'))
 	else isevars
       with _ -> isevars
-(*  	trace (str "decompose_prod_n failed"); *)
-(*  	raise (Invalid_argument "Subtac_coercion.inh_conv_coerces_to") *)
 end
diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml
index 24066d860e..78ee2f5cea 100644
--- a/contrib/subtac/subtac_pretyping.ml
+++ b/contrib/subtac/subtac_pretyping.ml
@@ -117,7 +117,6 @@ let env_with_binders env isevars l =
   in aux (env, []) l
 
 let subtac_process env isevars id bl c tycon =
-(*   let bl = Implicit_quantifiers.ctx_of_class_binders (vars_of_env env) cbl @ l in *)
   let c = Command.abstract_constr_expr c bl in
   let tycon = 
     match tycon with
@@ -132,12 +131,14 @@ let subtac_process env isevars id bl c tycon =
   let imps = Implicit_quantifiers.implicits_of_rawterm c in
   let coqc, ctyp = interp env isevars c tycon in
   let evm = non_instanciated_map env isevars (evars_of !isevars) in
-    evm, coqc, (match tycon with Some (None, c) -> c | _ -> ctyp), imps
+  let ty = nf_isevar !isevars (match tycon with Some (None, c) -> c | _ -> ctyp) in
+    evm, coqc, ty, imps
 
 open Subtac_obligations
 
 let subtac_proof kind env isevars id bl c tycon =
   let evm, coqc, coqt, imps = subtac_process env isevars id bl c tycon in
-  let evm = Subtac_utils.evars_of_term evm Evd.empty coqc in
-  let evars, def, ty = Eterm.eterm_obligations env id !isevars evm 0 coqc coqt in
+  let evm' = Subtac_utils.evars_of_term evm Evd.empty coqc in
+  let evm' = Subtac_utils.evars_of_term evm evm' coqt in
+  let evars, def, ty = Eterm.eterm_obligations env id !isevars evm' 0 coqc coqt in
     add_definition id def ty ~implicits:imps ~kind:kind evars
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
index 16180d1696..b5f9f99c1b 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -246,6 +246,8 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 		  uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
             ctxtv vdef in
 	evar_type_fixpoint loc env isevars names ftys vdefj;
+	let ftys = Array.map (nf_evar (evars_of !isevars)) ftys in
+	let fdefs = Array.map (fun x -> nf_evar (evars_of !isevars) (j_val x)) vdefj in
 	let fixj = match fixkind with
 	  | RFix (vn,i) ->
 	      (* First, let's find the guard indexes. *)
@@ -260,11 +262,11 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 		   | None -> list_map_i (fun i _ -> i) 0 ctxtv.(i))
 		vn)
 	      in 
-	      let fixdecls = (names,ftys,Array.map j_val vdefj) in 
+	      let fixdecls = (names,ftys,fdefs) in 
 	      let indexes = search_guard loc env possible_indexes fixdecls in 
 	      make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i)
 	  | RCoFix i -> 
-	      let cofix = (i,(names,ftys,Array.map j_val vdefj)) in
+	      let cofix = (i,(names,ftys,fdefs)) in
 	      (try check_cofix env cofix with e -> Stdpp.raise_with_loc loc e);
 	      make_judge (mkCoFix cofix) ftys.(i) in
 	inh_conv_coerce_to_tycon loc env isevars fixj tycon
@@ -273,13 +275,15 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	inh_conv_coerce_to_tycon loc env isevars (pretype_sort s) tycon
 
     | RApp (loc,f,args) -> 
-	let length = List.length args in	 
+	let length = List.length args in 
 	let ftycon = 
-	  match tycon with
-	      None -> None
+	  if length > 0 then
+	    match tycon with
+	    | None -> None
 	    | Some (None, ty) -> mk_abstr_tycon length ty
 	    | Some (Some (init, cur), ty) ->
 		Some (Some (length + init, length + cur), ty)
+	  else tycon
 	in
 	let fj = pretype ftycon env isevars lvar f in
  	let floc = loc_of_rawconstr f in
@@ -291,23 +295,13 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
               let resty = whd_betadeltaiota env (evars_of !isevars) resj.uj_type in
       		match kind_of_term resty with
 		  | Prod (na,c1,c2) ->
-		      let hj = pretype (mk_tycon c1) env isevars lvar c in
+		      Option.iter (fun ty -> isevars :=
+			Coercion.inh_conv_coerces_to loc env !isevars resty ty) tycon;
+		      let evd, (_, _, tycon) = split_tycon loc env !isevars tycon in
+		      isevars := evd;
+		      let hj = pretype (mk_tycon (nf_isevar !isevars c1)) env isevars lvar c in
 		      let value, typ = applist (j_val resj, [j_val hj]), subst1 hj.uj_val c2 in
 		      let typ' = nf_isevar !isevars typ in
-		      let tycon = 
-			Option.map 
-			  (fun (abs, ty) ->
-			     match abs with
-				 None ->
-				   isevars := Coercion.inh_conv_coerces_to loc env !isevars typ'
-				     (abs, ty);
-				   (abs, ty)
-			       | Some (init, cur) ->
-				   isevars := Coercion.inh_conv_coerces_to loc env !isevars typ' 
-				     (abs, ty);
-				   (Some (init, pred cur), ty))
-			  tycon
-		      in 
 			apply_rec env (n+1) 
 			  { uj_val = nf_isevar !isevars value;
 			    uj_type = nf_isevar !isevars typ' }
@@ -319,7 +313,6 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 			  (join_loc floc argloc) env (evars_of !isevars)
 	      		  resj [hj]
 	in
-	let ftycon = Option.map (lift_abstr_tycon_type (-1)) ftycon in
 	let resj = j_nf_evar (evars_of !isevars) (apply_rec env 1 fj ftycon args) in
 	let resj =
 	  match kind_of_term resj.uj_val with
@@ -332,12 +325,22 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	  inh_conv_coerce_to_tycon loc env isevars resj tycon
 
     | RLambda(loc,name,k,c1,c2)      ->
-	let (name',dom,rng) = evd_comb1 (split_tycon loc env) isevars tycon in
+	let tycon' = evd_comb1 
+	  (fun evd tycon -> 
+	    match tycon with 
+	    | None -> evd, tycon 
+	    | Some ty -> 
+		let evd, ty' = Coercion.inh_coerce_to_prod loc env evd ty in
+		  evd, Some ty') 
+	  isevars tycon 
+	in
+	let (name',dom,rng) = evd_comb1 (split_tycon loc env) isevars tycon' in
 	let dom_valcon = valcon_of_tycon dom in
 	let j = pretype_type dom_valcon env isevars lvar c1 in
 	let var = (name,None,j.utj_val) in
 	let j' = pretype rng (push_rel var env) isevars lvar c2 in 
-	  judge_of_abstraction env name j j'
+	let resj = judge_of_abstraction env name j j' in
+	  inh_conv_coerce_to_tycon loc env isevars resj tycon
 
     | RProd(loc,name,k,c1,c2)        ->
 	let j = pretype_type empty_valcon env isevars lvar c1 in
diff --git a/contrib/subtac/test/ListsTest.v b/contrib/subtac/test/ListsTest.v
index 3ceea173fe..05fc0803fc 100644
--- a/contrib/subtac/test/ListsTest.v
+++ b/contrib/subtac/test/ListsTest.v
@@ -1,5 +1,5 @@
 (* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *)
-Require Import Coq.subtac.Utils.
+Require Import Coq.Program.Program.
 Require Import List.
 
 Set Implicit Arguments.
@@ -7,7 +7,7 @@ Set Implicit Arguments.
 Section Accessors.
   Variable A : Set.
 
-  Program Definition myhd : forall { l : list A | length l <> 0 }, A :=  
+  Program Definition myhd : forall (l : list A | length l <> 0), A :=  
     fun l =>
       match l with
         | nil => !
@@ -39,7 +39,7 @@ Section app.
 
   Next Obligation.
     intros.
-    destruct_call app ; subtac_simpl.
+    destruct_call app ; program_simpl.
   Defined.
   
   Program Lemma app_id_l : forall l : list A, l = nil ++ l.
@@ -49,7 +49,7 @@ Section app.
   
   Program Lemma app_id_r : forall l : list A, l = l ++ nil.
   Proof.
-    induction l ; simpl ; auto.
+    induction l ; simpl in * ; auto. 
     rewrite <- IHl ; auto.
   Qed.
 
@@ -70,16 +70,24 @@ Section Nth.
 
   Next Obligation.
   Proof.
-    intros.
-    inversion H.
+    simpl in *. auto with arith. 
   Defined.
 
+  Next Obligation.
+  Proof.
+    inversion H.
+  Qed.
+
   Program Fixpoint nth' (l : list A) (n : nat | n < length l) { struct l } : A := 
     match l, n with
       | hd :: _, 0 => hd
       | _ :: tl, S n' => nth' tl n'
       | nil, _ => !
     end.
+  Next Obligation.
+  Proof.
+    simpl in *. auto with arith. 
+  Defined.
 
   Next Obligation.
   Proof.
diff --git a/contrib/subtac/test/take.v b/contrib/subtac/test/take.v
index 87ab47d639..2e17959c3e 100644
--- a/contrib/subtac/test/take.v
+++ b/contrib/subtac/test/take.v
@@ -1,9 +1,12 @@
 (* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *)
 Require Import JMeq.
 Require Import List.
-Require Import Coq.subtac.Utils.
+Require Import Program.
 
 Set Implicit Arguments.
+Obligations Tactic := idtac.
+
+Print cons.
 
 Program Fixpoint take (A : Set) (l : list A) (n : nat | n <= length l) { struct l } : { l' : list A | length l' = n } :=
   match n with
@@ -16,21 +19,14 @@ Program Fixpoint take (A : Set) (l : list A) (n : nat | n <= length l) { struct
   end.
 
 Require Import Omega.
-
+Solve All Obligations.
 Next Obligation.
-  intros.
-  simpl in l0.
-  apply le_S_n ; exact l0.
-Defined.
-
-Next Obligation.
-  intros.
-  destruct_call take ; subtac_simpl.
+  destruct_call take ; program_simpl.
 Defined.
 
 Next Obligation.
   intros.
-  inversion l0.
+  inversion H.
 Defined.
 
 
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index a8af39bc71..4ff60b41f2 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -43,6 +43,10 @@ module type S = sig
   val inh_coerce_to_base : loc ->
     env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_judgment
     
+  (* [inh_coerce_to_prod env isevars t] coerces [t] to a product type *)
+  val inh_coerce_to_prod : loc ->
+    env -> evar_defs -> type_constraint_type -> evar_defs * type_constraint_type
+
   (* [inh_conv_coerce_to loc env evd j t] coerces [j] to an object of type 
      [t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and
      [j.uj_type] are convertible; it fails if no coercion is applicable *)
@@ -160,6 +164,8 @@ module Default = struct
 
   let inh_coerce_to_base loc env evd j = (evd, j)
 
+  let inh_coerce_to_prod loc env evd t = (evd, t)
+
   let inh_coerce_to_fail env evd rigidonly v t c1 =
     if rigidonly & not (Heads.is_rigid env c1 && Heads.is_rigid env t)
     then
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index 00735d8746..ff33d679df 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -39,6 +39,10 @@ module type S = sig
      type its base type (the notion depends on the coercion system) *)
   val inh_coerce_to_base : loc ->
     env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_judgment
+
+  (* [inh_coerce_to_prod env isevars t] coerces [t] to a product type *)
+  val inh_coerce_to_prod : loc ->
+    env -> evar_defs -> type_constraint_type -> evar_defs * type_constraint_type
     
   (* [inh_conv_coerce_to loc env isevars j t] coerces [j] to an object of type 
      [t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 12826851f2..778fb3f0ea 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -1183,11 +1183,12 @@ let split_tycon loc env evd tycon =
 		 if cur = 0 then 
 		   let evd', (x, dom, rng) = real_split c in
 		     evd, (Anonymous, 
-			       Some (Some (init, 0), dom), 
-			       Some (Some (init, 0), rng))
+			  Some (None, dom), 
+			  Some (None, rng))
 		 else
-		   evd, (Anonymous, None, Some (Some (init, pred cur), c)))
-
+		   evd, (Anonymous, None, 
+			Some (if cur = 1 then None,c else Some (init, pred cur), c)))
+	    
 let valcon_of_tycon x = 
   match x with
     | Some (None, t) -> Some t
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 11d3b37104..17c7efb457 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -356,7 +356,9 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		   uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
             ctxtv vdef in
 	evar_type_fixpoint loc env evdref names ftys vdefj;
-	let fixj = match fixkind with
+	let ftys = Array.map (nf_evar (evars_of !evdref)) ftys in
+	let fdefs = Array.map (fun x -> nf_evar (evars_of !evdref) (j_val x)) vdefj in
+ 	let fixj = match fixkind with
 	  | RFix (vn,i) ->
 	      (* First, let's find the guard indexes. *)
 	      (* If recursive argument was not given by user, we try all args.
@@ -370,11 +372,11 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		   | None -> list_map_i (fun i _ -> i) 0 ctxtv.(i))
 		vn)
 	      in 
-	      let fixdecls = (names,ftys,Array.map j_val vdefj) in 
+	      let fixdecls = (names,ftys,fdefs) in 
 	      let indexes = search_guard loc env possible_indexes fixdecls in 
 	      make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i)
 	  | RCoFix i ->
-	      let cofix = (i,(names,ftys,Array.map j_val vdefj)) in
+	      let cofix = (i,(names,ftys,fdefs)) in
 	      (try check_cofix env cofix with e -> Stdpp.raise_with_loc loc e);
 	      make_judge (mkCoFix cofix) ftys.(i) in
 	inh_conv_coerce_to_tycon loc env evdref fixj tycon