Imported Upstream version 8.1~gammaupstream/8.1.gamma

1 files changed, 43 insertions, 29 deletions

diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index d4db7c27..7b96758a 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -80,25 +80,34 @@ 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_named_context = Termops.print_named_context
 let my_print_env = Termops.print_env
 let my_print_rawconstr = Printer.pr_rawconstr_env
 let my_print_evardefs = Evd.pr_evar_defs
 
 let my_print_tycon_type = Evarutil.pr_tycon_type
 
-let debug_level = 2
+let debug_level = 1
+
+let debug_on = true
 
 let debug n s = 
-  if !Options.debug && n >= debug_level then
-    msgnl s
+  if debug_on then
+    if !Options.debug && n >= debug_level then
+      msgnl s
+    else ()
   else ()
 
 let debug_msg n s = 
-  if !Options.debug  && n >= debug_level then s
+  if debug_on then
+    if !Options.debug  && n >= debug_level then s
+    else mt ()
   else mt ()
 
 let trace s = 
-  if !Options.debug  && debug_level > 0 then msgnl s
+  if debug_on then
+    if !Options.debug  && debug_level > 0 then msgnl s
+    else ()
   else ()
 
 let wf_relations = Hashtbl.create 10
@@ -167,30 +176,6 @@ let goal_fix_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Fixp
 open Tactics
 open Tacticals
 
-let build_dependent_sum l =
-  let rec aux (tac, typ) = function
-      (n, t) :: tl ->
-	let t' = mkLambda (Name n, t, typ) in
-	  trace (spc () ++ str ("treating evar " ^ string_of_id n));
-	  (try trace (str " assert: " ++ my_print_constr (Global.env ()) t)	    	     
-	   with _ -> ());
-	let tac' = 
-	  tclTHENS (assert_tac true (Name n) t) 
-	    ([intros;
-	      (tclTHENSEQ 
-		 [constructor_tac (Some 1) 1 
-		    (Rawterm.ImplicitBindings [mkVar n]);
-		  tac]);
-	     ])
-	in
-	let newt = mkApp (Lazy.force ex_ind, [| t; t'; |]) in
-	  aux (tac', newt) tl
-    | [] -> tac, typ
-  in 
-    match l with 
-	(_, hd) :: tl -> aux (intros, hd) tl
-      | [] -> raise (Invalid_argument "build_dependent_sum")
-
 let id x = x
 
 let build_dependent_sum l =
@@ -438,3 +423,32 @@ let rewrite_cases env c =
   let c' = rewrite_cases c in
   let _ = trace (str "Rewrote cases: " ++ spc () ++ my_print_rawconstr env c') in
     c'
+
+let id_of_name = function
+    Name n -> n
+  | Anonymous -> raise (Invalid_argument "id_of_name")
+
+let definition_message id =
+  Options.if_verbose message ((string_of_id id) ^ " is defined")
+
+let recursive_message v =
+  match Array.length v with
+    | 0 -> error "no recursive definition"
+    | 1 -> (Printer.pr_global v.(0) ++ str " is recursively defined")
+    | _ -> hov 0 (prvect_with_sep pr_coma Printer.pr_global v ++
+		    spc () ++ str "are recursively defined")
+
+(* Solve an obligation using tactics, return the corresponding proof term *)
+let solve_by_tac ev t =
+  debug 1 (str "Solving goal using tactics: " ++ Evd.pr_evar_info ev);
+  let goal = Proof_trees.mk_goal ev.evar_hyps ev.evar_concl None in
+  let ts = Tacmach.mk_pftreestate goal in
+  let solved_state = Tacmach.solve_pftreestate t ts in
+  let c = Tacmach.extract_pftreestate solved_state in
+    debug 1 (str "Term constructed in solve by tac: " ++ my_print_constr (Global.env ()) c);
+    c
+
+let rec string_of_list sep f = function
+    [] -> ""
+  | x :: [] -> f x
+  | x :: ((y :: _) as tl) -> f x ^ sep ^ string_of_list sep f tl