Latest fixes, should work fine now for non recursive definitions, although still has some syntax problems

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

5 files changed, 56 insertions, 34 deletions

diff --git a/contrib/subtac/context.ml b/contrib/subtac/context.ml
index 9ea5e75019..236b0ea534 100644
--- a/contrib/subtac/context.ml
+++ b/contrib/subtac/context.ml
@@ -16,13 +16,7 @@ let assoc_and_index x l =
 let id_of_name = function
     Name id -> id
   | Anonymous -> raise (Invalid_argument "id_of_name")
-
-let rel_to_vars ctx constr =
-  let rec aux acc = function
-      (n, _, _) :: ctx -> 
-	aux (Term.subst1 (mkVar n) acc) ctx
-    | [] -> acc
-  in aux constr ctx
+(*
 
 let subst_ctx ctx c = 
   let rec aux ((ctx, n, c) as acc) = function
@@ -36,12 +30,6 @@ let subst_ctx ctx c =
   in 
   let (x, _, z) = aux ([], pred (List.length ctx), c) (List.rev ctx) in 
     (x, rel_to_vars x z)
-	
-let names_context_of ctx = 
-  List.map (fun (x, _, _) -> x) ctx
-
-let env_of_ctx env (ctx : t) = 
-  Environ.push_rel_context ctx env
-
+*)
 
 let subst_env env c = (env, c)
diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
index e59dead344..3574cfeae8 100644
--- a/contrib/subtac/eterm.ml
+++ b/contrib/subtac/eterm.ml
@@ -11,6 +11,10 @@ open Evd
 open List
 open Pp
 
+let reverse_array arr = 
+  Array.of_list (List.rev (Array.to_list arr))
+    
+
 (** Utilities to find indices in lists *)
 let list_index x l =
   let rec aux i = function
@@ -39,8 +43,8 @@ let subst_evars evs n t =
 (* 	     mkVar (id_of_string ("Evar" ^ string_of_int k));*)
   	     mkRel (evar_index k + depth)  
 	   in
-	   let args = Array.map (map_constr_with_binders succ substrec depth) args in
-	     mkApp (ex, args)
+	   let args = List.rev_map (map_constr_with_binders succ substrec depth) (Array.to_list args) in
+	     mkApp (ex, Array.of_list args)
 	 with Not_found -> 
 	   msgnl (str "Evar " ++ int k ++ str " not found!!!");
 	   c)
diff --git a/contrib/subtac/interp.ml b/contrib/subtac/interp.ml
index 83f26ced1e..3b638df021 100644
--- a/contrib/subtac/interp.ml
+++ b/contrib/subtac/interp.ml
@@ -656,11 +656,14 @@ let subtac' recursive id env (s, t) =
 	  Some t -> make_fixpoint t id realt
 	| None -> realt
     in
+      (try trace (str "Original evar map: " ++ Evd.pr_evar_map (evars_of !evd));
+       with Not_found -> trace (str "Not found in pr_evar_map"));
     let realt = Evarutil.nf_evar (evars_of !evd) realt in
+    let coqtype = Evarutil.nf_evar (evars_of !evd) coqtype in
     trace (str "Coq term: " ++ my_print_constr env realt ++ spc ()
 	   ++ str "Coq type: " ++ my_print_constr env coqtype);
     let evm = non_instanciated_map env nonimplicit evd in
-      (try trace (str "Original evar map: " ++ Evd.pr_evar_map evm);
+      (try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm);
        with Not_found -> trace (str "Not found in pr_evar_map"));
     let tac = Eterm.etermtac (evm, realt) in 
     msgnl (str "Starting proof");
@@ -700,10 +703,16 @@ let subtac' recursive id env (s, t) =
 		str "Uncoercible terms:" ++ spc ()
 		++ x ++ spc () ++ str "and" ++ spc () ++ y
 	in msg_warning cmds
-
+    
+    | Type_errors.TypeError (env, e) ->
+	debug 2 (Himsg.explain_type_error env e)
+	  
+    | Pretype_errors.PretypeError (env, e) ->
+	debug 2 (Himsg.explain_pretype_error env e)
+	  
     | e -> 
-	msg_warning (str "Uncatched exception: " ++ str (Printexc.to_string e))
-	(*raise e*)
+	msg_warning (str "Uncatched exception: " ++ str (Printexc.to_string e));
+	raise e
 
 let subtac recursive id env (s, t) =
   subtac' recursive id (Global.env ()) (s, t)
diff --git a/contrib/subtac/scoq.ml b/contrib/subtac/scoq.ml
index 1fbb0d7457..3e8bec6242 100644
--- a/contrib/subtac/scoq.ml
+++ b/contrib/subtac/scoq.ml
@@ -80,20 +80,35 @@ let app_opt c e =
     | None -> e	
 
 let make_existential loc env nonimplicit isevars c =
-  let key = mknewexist () in
-  let args = Sign.instance_from_named_context (Environ.named_context env) in
-    isevars :=
-      Evd.evar_declare (Environ.named_context_val env) key c ~src:(loc, InternalHole) !isevars;
+  let evar = Evarutil.e_new_evar isevars env ~src:(loc, QuestionMark) c in
+  let (key, args) = destEvar evar in
+    debug 2 (str "Constructed evar " ++ int key ++ str " applied to args: " ++
+	     Array.fold_right (fun a acc -> my_print_constr env a ++ spc () ++ acc) args (str ""));
     nonimplicit := Gset.add key !nonimplicit;
-    mkEvar(key, args)
-
+    evar
+
+let string_of_hole_kind = function
+  | ImplicitArg _ -> "ImplicitArg"
+  | BinderType _ -> "BinderType"
+  | QuestionMark -> "QuestionMark"
+  | CasesType -> "CasesType"
+  | InternalHole -> "InternalHole"
+  | TomatchTypeParameter _ -> "TomatchTypeParameter"
+      
 let non_instanciated_map env nonimplicit evd =
   let evm = evars_of !evd in
     List.fold_left 
       (fun evm (key, evi) -> 
-	 if Gset.mem key !nonimplicit then
-	   Evd.add evm key evi
-	 else
-	   let (loc,k) = evar_source key !evd in
-	     Pretype_errors.error_unsolvable_implicit loc env evm k)
+	 let (loc,k) = evar_source key !evd in
+	   debug 2 (str "evar " ++ int key ++ str " has kind " ++ 
+		    str (string_of_hole_kind k));
+	   if Gset.mem key !nonimplicit then
+	     begin
+	       debug 2 (str " and is not an implicit");
+	       Evd.add evm key evi
+	     end
+	   else
+	     let (loc,k) = evar_source key !evd in
+	       debug 2 (str " and is an implicit");
+	       Pretype_errors.error_unsolvable_implicit loc env evm k)
       Evd.empty (Evarutil.non_instantiated evm)
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index fa5dc5bec7..513842150c 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -99,12 +99,18 @@ let rec mu env isevars t =
 and coerce loc env nonimplicit isevars (x : Term.constr) (y : Term.constr) 
     : (Term.constr -> Term.constr) option 
     =
+  trace (str "Coerce called for " ++ (my_print_constr env x) ++ 
+	 str " and "++ my_print_constr env y);
+
   let rec coerce_unify env x y =
-    if e_cumul env isevars x y then None
-    else coerce' env x y (* head recutions needed *)
+    if e_cumul env isevars x y then (
+      trace (str "Unified " ++ (my_print_constr env x) ++ 
+	     str " and "++ my_print_constr env y);
+      None
+    ) else coerce' env x y (* head recutions needed *)
   and coerce' env x y : (Term.constr -> Term.constr) option =
     let subco () = subset_coerce env x y in
-      trace (str "Coercion from " ++ (my_print_constr env x) ++ 
+      trace (str "coerce' from " ++ (my_print_constr env x) ++ 
 	     str " to "++ my_print_constr env y);
       match (kind_of_term x, kind_of_term y) with
 	| Sort s, Sort s' ->