Actual fix for the unification problem in theories/Reals/Rtrigo_fun (previous and current version work).

Changed the type of typing constraints so as to have all the necessary information on abstract tycons.
Updates of subtac to use the new type.



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

4 files changed, 55 insertions, 43 deletions

diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index 4b4a25e718..e0d779ca38 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -429,21 +429,22 @@ module Coercion = struct
 	      Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++
 	      Termops.print_env env);
      with _ -> ());
-    if n = 0 then
-      let (evd', val', type') = 
-	try 
-	  inh_conv_coerce_to_fail loc env isevars (Some cj.uj_val) cj.uj_type t
-	with NoCoercion ->
-	  let sigma = evars_of isevars in
-	    try
-	      coerce_itf loc env isevars (Some cj.uj_val) cj.uj_type t
-	    with NoSubtacCoercion ->
-	      error_actual_type_loc loc env sigma cj t
-      in
-      let val' = match val' with Some v -> v | None -> assert(false) in
-	(evd',{ uj_val = val'; uj_type = t })
-    else
-      (isevars, cj)
+    match n with
+	None ->
+	  let (evd', val', type') = 
+	    try 
+	      inh_conv_coerce_to_fail loc env isevars (Some cj.uj_val) cj.uj_type t
+	    with NoCoercion ->
+	      let sigma = evars_of isevars in
+		try
+		  coerce_itf loc env isevars (Some cj.uj_val) cj.uj_type t
+		with NoSubtacCoercion ->
+		  error_actual_type_loc loc env sigma cj t
+	  in
+	  let val' = match val' with Some v -> v | None -> assert(false) in
+	    (evd',{ uj_val = val'; uj_type = t })
+      | Some (init, cur) ->
+	  (isevars, cj)
 
   let inh_conv_coerces_to loc env isevars t ((abs, t') as tycon) =
     (try 
@@ -453,20 +454,25 @@ module Coercion = struct
 	      Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++
 	      Termops.print_env env);
      with _ -> ());
+    let nabsinit, nabs = 
+      match abs with
+	  None -> 0, 0
+	| Some (init, cur) -> init, cur
+    in
     let (rels, rng) = 
       (* a little more effort to get products is needed *) 
-      try decompose_prod_n abs t
+      try decompose_prod_n nabs t
       with _ -> 
 	trace (str "decompose_prod_n failed");
 	raise (Invalid_argument "Subtac_coercion.inh_conv_coerces_to")
     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 abs) rng then (
-	trace (str "No occur between 0 and " ++ int (succ abs));
+      if noccur_with_meta 0 (succ (nabsinit - nabs)) rng then (
+	trace (str "No occur between 0 and " ++ int (succ (nabsinit - nabs)));
 	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 abs t'
+	    env', rng, lift nabs t'
 	in
 	  try 
 	    pi1 (try inh_conv_coerce_to_fail loc env' isevars None t t'
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index 94f2d70ac4..1b92c69110 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -56,6 +56,7 @@ let interp_gen kind isevars env
                c =
   let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_soapp ~ltacvars (Evd.evars_of !isevars) env c in
   let c' = Subtac_interp_fixpoint.rewrite_cases env c' in
+    msgnl (str "Pretyping " ++ my_print_constr_expr c);
   let c' = SPretyping.pretype_gen isevars env ([],[]) kind c' in
     evar_nf isevars c'
     
@@ -69,9 +70,10 @@ let interp_casted_constr isevars env ?(impls=([],[])) c typ =
   interp_gen (OfType (Some typ)) isevars env ~impls c 
 
 let interp_open_constr isevars env c =
-  let c = SPretyping.pretype_gen isevars env ([], []) (OfType None) 
-	    (Constrintern.intern_constr (Evd.evars_of !isevars) env c) in
-    evar_nf isevars c
+    msgnl (str "Pretyping " ++ my_print_constr_expr c);
+  let c = Constrintern.intern_constr (Evd.evars_of !isevars) env c in
+  let c' = SPretyping.pretype_gen isevars env ([], []) (OfType None) c in
+    evar_nf isevars c'
 
 let interp_constr_judgment isevars env c =
   let j = 
@@ -204,22 +206,22 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
 			       Ppconstr.pr_constr_expr body)
 		in
 		let env', binders_rel = interp_context isevars env0 bl in
-		let before, ((argname, _, argtyp) as arg), after = list_chop_hd n binders_rel in
+		let after, ((argname, _, argtyp) as arg), before = list_chop_hd n binders_rel in
 		let argid = match argname with Name n -> n | _ -> assert(false) in
 		let after' = List.map (fun (n, c, t) -> (n, option_app (lift 1) c, lift 1 t)) after in
 		let envwf = push_rel_context before env0 in
 		let wf_rel = interp_constr isevars envwf r in
 		let accarg_id = id_of_string ("Acc_" ^ string_of_id argid) in
-		let accarg = (Name accarg_id, None, mkApp (Lazy.force acc_inv, [| wf_rel; mkRel 1 |])) in
+		let accarg = (Name accarg_id, None, mkApp (Lazy.force acc_inv, [| argtyp; wf_rel; mkRel 1 |])) in
 		let argid' = id_of_string (string_of_id argid ^ "'") in
 		let before_length, after_length = List.length before, List.length after in
 		let full_length = before_length + 1 + after_length in
-		let wfarg = (Name argid, None, 
-			     mkSubset (Name argid') argtyp 
-			       (mkApp (wf_rel, [|mkRel 1; mkRel (full_length + 1)|])))
+		let wfarg len = (Name argid, None, 
+				 mkSubset (Name argid') argtyp 
+				   (mkApp (wf_rel, [|mkRel 1; mkRel (len + 1)|])))
 		in
-		let new_bl = before @ (arg :: accarg :: after')
-		and intern_bl =  before @ (wfarg :: after)
+		let new_bl = after' @ (accarg :: arg :: before)
+		and intern_bl =  after @ (wfarg (before_length + 1) :: before)
 		in
 		let intern_env = push_rel_context intern_bl env0 in
 		let env' = push_rel_context new_bl env0 in
@@ -227,7 +229,15 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
 		let intern_arity = it_mkProd_or_LetIn arity intern_bl in
 		let arity' = interp_type isevars env' arityc in
 		let arity' = it_mkProd_or_LetIn arity' new_bl in
-		let fun_bl = before @ (arg :: (Name recname, None, arity) :: after') in
+		let fun_bl = after @ ((Name recname, None, intern_arity) :: arg :: before) in
+		let _ = 
+		  let pr c = my_print_constr env c in
+		  let prr = Printer.pr_rel_context env in
+		    trace (str "Fun bl: " ++ prr fun_bl ++ spc () ++
+			     str "Intern bl" ++ prr intern_bl ++ spc () ++
+			     str "Extern bl" ++ prr new_bl ++ spc () ++
+			     str "Intern arity: " ++ pr intern_arity)
+		in
 		let impl = 
 		  if Impargs.is_implicit_args()
 		  then Impargs.compute_implicits intern_env arity'
@@ -256,11 +266,11 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
 		   let def = abstract_constr_expr def bl in
 		     isevars, info, interp_casted_constr isevars rec_sign ~impls:([],rec_impls)
 		       def arity
-	       | Some (n, artyp, wfrel, bl, intern_bl, intern_arity) ->
-		   let rec_sign = push_rel_context bl rec_sign in
+	       | Some (n, artyp, wfrel, fun_bl, intern_bl, intern_arity) ->
+		   let rec_sign = push_rel_context fun_bl rec_sign in
 		   let cstr = interp_casted_constr isevars rec_sign ~impls:([],rec_impls)
 				def intern_arity
-		   in isevars, info, cstr)
+		   in isevars, info, it_mkLambda_or_LetIn cstr fun_bl)
           lnameargsardef arityl
       with e ->
 	States.unfreeze fs; raise e in
@@ -328,19 +338,13 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
       let evm = Evd.evars_of isevars in
       let _, _, typ = arrec.(i) in
       let id = namerec.(i) in
-      let def = 
-	match info with 
-	    Some (n, artyp, wfrel, funbl, bl, arity) ->
-	      def (* mkApp (def, *)
-
-	  | None -> def
-		     in
-	(* Generalize by the recursive prototypes  *)
+      let evars_def, evars_typ, evars = Eterm.eterm_term evm def (Some typ) in 	
+      (* Generalize by the recursive prototypes  *)
       let def = 
 	Termops.it_mkNamedLambda_or_LetIn def (Environ.named_context rec_sign)
       and typ = 
-	Termops.it_mkNamedProd_or_LetIn typ (Environ.named_context rec_sign) in
-      let evars_def, evars_typ, evars = Eterm.eterm_term evm def (Some typ) in 
+	Termops.it_mkNamedProd_or_LetIn typ (Environ.named_context rec_sign) 
+      in
       (*let evars_typ = match evars_typ with Some t -> t | None -> assert(false) in*)
       (*let fi = id_of_string (string_of_id id ^ "_evars") in*)
       (*let ce = 
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index d620c8e9fa..6c165dada1 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -74,6 +74,7 @@ let extsort s = Constrextern.extern_constr true (Global.env ()) (mkSort s)
 open Pp
 
 let my_print_constr = Termops.print_constr_env
+let my_print_constr_expr = Ppconstr.pr_constr_expr
 let my_print_context = Termops.print_rel_context
 let my_print_env = Termops.print_env
 let my_print_rawconstr = Printer.pr_rawconstr_env
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli
index a53016484b..92a995c891 100644
--- a/contrib/subtac/subtac_utils.mli
+++ b/contrib/subtac/subtac_utils.mli
@@ -47,6 +47,7 @@ val acc_inv : constr lazy_t
 val extconstr : constr -> constr_expr
 val extsort : sorts -> constr_expr
 val my_print_constr : env -> constr -> std_ppcmds
+val my_print_constr_expr : constr_expr -> std_ppcmds
 val my_print_evardefs : evar_defs -> std_ppcmds
 val my_print_context : env -> std_ppcmds
 val my_print_env : env -> std_ppcmds