Rewrite of the subtac tactic, needs some work on implicit arguments.

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

1 files changed, 0 insertions, 682 deletions

diff --git a/contrib/subtac/rewrite.ml b/contrib/subtac/rewrite.ml
deleted file mode 100644
index afbbd18af..000000000
--- a/contrib/subtac/rewrite.ml
+++ /dev/null
@@ -1,682 +0,0 @@
-open Evd
-open Libnames
-open Coqlib
-open Natural
-open Infer
-open Term
-open Names
-open Scoq
-open Pp
-open Printer
-open Util
-
-type recursion_info = {
-  arg_name: identifier;
-  arg_type: types; (* A *)
-  wf_relation: constr; (* R : A -> A -> Prop *)
-  wf_proof: constr; (* : well_founded R *)
-  f_type: types; (* f: A -> Set *)
-  f_fulltype: types; (* Type with argument and wf proof product first *)
-}
-
-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
-      (name, None, typ) :: tl -> 
-	aux (((id_of_name name, None, rel_to_vars ctx typ) :: ctx), 
-	     pred n, c) tl
-    | (name, Some term, typ) :: tl ->
-	let t' = Term.substnl [term] n c in
-	  aux (ctx, n, t') tl
-    | [] -> acc
-  in 
-  let (x, _, z) = aux ([], pred (List.length ctx), c) (List.rev ctx) in 
-    (x, rel_to_vars x z)
-	
-(* Anotation needed for failed generalization *)
-let named_context_of_ctx ctx : Sign.named_context = 
-  List.fold_right 
-    (fun (name, x, t) ctx -> 
-       let x' = match x with 
-	   Some e -> Some (rel_to_vars ctx e)
-	 | None -> None
-       and t' = rel_to_vars ctx t in
-	 (id_of_name name, x', t') :: ctx) 
-    ctx []
-    
-let env_of_ctx ctx : Environ.env =
-  Environ.push_rel_context ctx (Global.env ())
-
-let rels_of_ctx ctx = 
-  let n = List.length ctx in
-  Array.init n (fun i -> mkRel (n - i)) 
-
-type prog_info = {
-  mutable evm: evar_map;
-  rec_info: recursion_info option;
-}
-
-let my_print_constr ctx term =
-  Termops.print_constr_env (env_of_ctx ctx) term
-
-let my_print_context ctx = 
-  Termops.print_rel_context (env_of_ctx ctx)
-      
-let pair_of_array a = (a.(0), a.(1))
-let make_name s = Name (id_of_string s)
-
-let app_opt c e = 
-  match c with
-      Some constr -> constr e
-    | None -> e	
-
-(* Standard ? *)
-let unlift n c = 
-  let rec aux n acc =
-    if n = 0 then acc
-    else aux (pred n) (Termops.pop acc)
-  in aux n c
-
-let filter_defs l = List.filter (fun (_, c, _) -> c = None) l
-
-let evar_args ctx = 
-  let n = List.length ctx in
-  let rec aux acc i = function
-      (_, c, _) :: tl ->
-	(match c with
-	   | None -> aux (mkRel i :: acc) (succ i) tl
-	   | Some _ -> aux acc (succ i) tl)
-    | [] -> acc
-  in Array.of_list (aux [] 1 ctx)
-      
-let evar_ctx prog_info ctx = 
-  let ctx' = 
-    match prog_info.rec_info with
-      Some ri ->
-	let len = List.length ctx in
-	assert(len >= 2);
-	let rec aux l acc = function
-	    0 ->
-	      (match l with
-		   (id, _, recf) :: arg :: [] -> arg :: (id, None, ri.f_fulltype) :: acc
-		 | _ -> assert(false))
-	  | n -> (match l with
-		      hd :: tl -> aux tl (hd :: acc) (pred n)
-		    | _ -> assert(false))
-	in
-	  List.rev (aux ctx [] (len - 2))	    
-    | None -> ctx
-  in filter_defs ctx'
-
-let if_branches c = 
-  match kind_of_term c with
-    | App (c, l) ->
-	(match kind_of_term c with
-	     Ind i ->
-	       let len = Array.length l in
-		 if len = 2
-		 then
-		   let (a, b) = pair_of_array l in
-		     Some (i, (a,b))
-		 else None
-	   | _ -> None)
-    | _ -> None
-
-let disc_proj_exist ctx x =
-  trace (str "disc_proj_exist: " ++ my_print_constr ctx x);
-  match kind_of_term x with
-    | App (c, l) ->
-	(if Term.eq_constr c (Lazy.force sig_).proj1 
-	   && Array.length l = 3 
-	 then
-	   (match kind_of_term l.(2) with
-	        App (c, l) ->
-		  (match kind_of_term c with
-		       Construct c ->
-			 if c = Term.destConstruct (Lazy.force sig_).intro
-			   && Array.length l = 4
-			 then
-			   Some (l.(0), l.(1), l.(2), l.(3))
-			 else None
-		     | _ -> None)
-	       | _ -> None)
-	 else None)
-    | _ -> None
-      
-let rec rewrite_type prog_info ctx ((loc, t) as lt) : Term.types * Term.types =
-  trace (str "rewrite_type: " ++ print_dtype_loc [] lt);
-  trace (str "context: " ++ my_print_context ctx);
-  let aux prog_info ctx x = fst (rewrite_type prog_info ctx x) in
-    match t with
-	DTPi ((name, a), b, s) -> 
-	  let ta = aux prog_info ctx a in
-	  let ctx' = (snd name, None, ta) :: ctx in
-	    (mkProd (snd name, ta, aux prog_info ctx' b)), mkSort (snd s)
-	    
-      | DTSigma ((name, a), b, s) ->
-	  let ta = aux prog_info ctx a in
-	  let ctx' = (snd name, None, ta) :: ctx in
-	    mkApp ((Lazy.force existS).typ, 
-		   [| ta; 
-		      mkLambda 
-			(snd name, ta, aux prog_info ctx' b) |]),
-	  mkSort (snd s)
-	    
-      | DTSubset ((name, a), b, s) -> 
-	  let ta = aux prog_info ctx a in
-	  let name = Name (snd name) in
-	  let ctx' = (name, None, ta) :: ctx in
-	    (mkApp ((Lazy.force sig_).typ, 
-		    [| ta; mkLambda (name, ta, aux prog_info ctx' b) |])),
-	  mkSort (snd s)
-	      
-      | DTRel i -> 
-	  let (_, term, typ) = List.nth ctx i in
-	  let t = 
-	    (*match term with
-		Some t -> Term.lift (succ i) t
-	      | None -> *)mkRel (succ i)
-	  in t, Term.lift (succ i) typ
-	    
-      | DTApp (x, y, t, _) -> 
-	  let (cx, tx), (cy, ty) = 
-	    rewrite_type prog_info ctx x, rewrite_type prog_info ctx y 
-	  in
-	  let coercex, coqx = mutype prog_info ctx tx in
-	  let narg, targ, tres =
-	    match decompose_prod_n 1 coqx with
-		[x, y], z -> x, y, z
-	      | _ -> assert(false)
-	  in	    
-	    debug 2 (str "Coercion for type application: " ++
-		       my_print_constr ctx cx ++ spc () 
-		     ++ my_print_constr ctx cy);
-	  let coercey = coerce prog_info ctx ty targ in
-	  let t' = Term.subst1 (app_opt coercey cy) tres in
-	  let term = mkApp (app_opt coercex cx, [|app_opt coercey cy|]) in
-	    debug 1 (str "Term obtained after coercion (at application): " ++
-		       my_print_constr ctx term);
-	    term, t'
-	      
-      | DTCoq (t, dt, _) -> 
-	  (* type should be equivalent to 'aux prog_info ctx dt' *)
-	  t, Typing.type_of (env_of_ctx ctx) prog_info.evm t 
-      | DTTerm (t, dt, _) -> rewrite_term prog_info ctx t
-      | DTSort s -> mkSort (snd s), mkSort type_0 (* false *)
-      | DTInd (_, t, i, s) -> 
-	  let (_, ind) = Inductive.lookup_mind_specif (Global.env ()) i in
-	    mkInd i, ind.Declarations.mind_nf_arity
-	  
-and mutype prog_info ctx t = 
-  match disc_subset t with
-      Some (u, p) -> 
-	let f, ct = mutype prog_info ctx u in
-	  (Some (fun x ->		   
-		   app_opt f (mkApp ((Lazy.force sig_).proj1, 
-				     [| u; p; x |]))),
-	   ct)
-    | None -> (None, t)
-
-and muterm prog_info ctx t = mutype prog_info ctx t
-
-and coerce' prog_info ctx x y : (Term.constr -> Term.constr) option =
-  let subco () = subset_coerce prog_info ctx x y in
-    trace (str "Coercion from " ++ (my_print_constr ctx x) ++ 
-	     str " to "++ my_print_constr ctx y);
-  match (kind_of_term x, kind_of_term y) with
-    | Sort s, Sort s' -> 
-	(match s, s' with
-	     Prop x, Prop y when x = y -> None
-	   | Prop _, Type _ -> None
-	   | Type x, Type y when x = y -> None (* false *)
-	   | _ -> subco ())
-    | Prod (name, a, b), Prod (name', a', b') ->
-	let c1 = coerce prog_info ctx a' a in
-	let bsubst = Term.subst1 (app_opt c1 (mkRel 1)) b in
-	let c2 = coerce prog_info ((name', None, a') :: ctx) bsubst b' in
-	  (match c1, c2 with
-	       None, None -> None
-	     | _, _ ->
-		 Some
-		   (fun f -> 
-		      mkLambda (name', a',
-				app_opt c2
-				  (mkApp (Term.lift 1 f, 
-					  [| app_opt c1 (mkRel 1) |])))))
-
-    | App (c, l), App (c', l') ->
-	(match kind_of_term c, kind_of_term c' with
-	     Ind i, Ind i' ->
-	       let len = Array.length l in
-	       let existS = Lazy.force existS and sig_ = Lazy.force sig_ in
-		 if len = Array.length l' && len = 2
-		   && i = i' && i = Term.destInd existS.typ 
-		 then
-		   begin (* Sigma types *)
-		     debug 1 (str "In coerce sigma types");
-		     let (a, pb), (a', pb') = 
-		       pair_of_array l, pair_of_array l' 
-		     in
-		     let c1 = coerce prog_info ctx a a' in
-		     let remove_head c = 
-		       let (_, _, x) = Term.destProd c in
-			 x
-		     in
-		     let b, b' = remove_head pb, remove_head pb' in
-		     let b'subst = 
-		       match c1 with
-			   None -> b' 
-			 | Some c1 -> Term.subst1 (c1 (mkRel 1)) b' 
-		     in
-		     let ctx' = (make_name "x", None, a) :: ctx in
-		     let c2 = coerce prog_info ctx' b b'subst in
-		       match c1, c2 with
-			   None, None -> None
-			 | _, _ ->
-			     Some 
-			       (fun x ->
-				  let x, y = 
-				    app_opt c1 (mkApp (existS.proj1,
-						       [| a; pb; x |])),
-				    app_opt c2 (mkApp (existS.proj2, 
-						       [| a; pb'; x |]))
-				  in
-				    mkApp (existS.intro, [| x ; y |]))
-		   end
-		 else subco ()
-	   | _ ->  subco ())
-    | _, _ ->  subco ()
-
-and coerce prog_info ctx (x : Term.constr) (y : Term.constr) 
-    : (Term.constr -> Term.constr) option 
-    =
-  try let cstrs = Reduction.conv_leq (Global.env ()) x y in None
-  with Reduction.NotConvertible -> coerce' prog_info ctx x y
-      
-and disc_subset x = 
-  match kind_of_term x with
-    | App (c, l) ->
-	(match kind_of_term c with
-	     Ind i ->
-	       let len = Array.length l in
-	       let sig_ = Lazy.force sig_ in
-		 if len = 2 && i = Term.destInd sig_.typ
-		 then
-		   let (a, b) = pair_of_array l in
-		     Some (a, b)
-		 else None
-	   | _ -> None)
-    | _ -> None
-	
-and disc_exist ctx x =
-  trace (str "Disc_exist: " ++ my_print_constr ctx x);
-  match kind_of_term x with
-    | App (c, l) ->
-	(match kind_of_term c with
-	     Construct c ->	       
-	       if c = Term.destConstruct (Lazy.force sig_).intro
-	       then Some (l.(0), l.(1), l.(2), l.(3))
-	       else None
-	   | _ -> None)
-    | _ -> None
-       
-and subset_coerce prog_info ctx x y =
-  match disc_subset x with
-      Some (u, p) -> 
-	let c = coerce prog_info ctx u y in
-	let f x = 
-	  app_opt c (mkApp ((Lazy.force sig_).proj1, 
-			    [| u; p; x |]))
-	in Some f
-    | None ->
-	match disc_subset y with
-	    Some (u, p) ->
-	      let c = coerce prog_info ctx x u in
-	      let t = id_of_string "t" in
-	      let evarinfo x =
-		let cx = app_opt c x in
-		let pcx = mkApp (p, [| cx |]) in
-		let ctx', pcx' = subst_ctx ctx pcx in
-		  cx, {
-		    Evd.evar_concl = pcx';
-		    Evd.evar_hyps = 
-                     Environ.val_of_named_context (evar_ctx prog_info ctx');
-		    Evd.evar_body = Evd.Evar_empty;
-		  }
-	      in
-		Some 
-		  (fun x ->
-		     let key = mknewexist () in
-		     let cx, evi = evarinfo x in
-		       prog_info.evm <- Evd.add prog_info.evm key evi;
-		       (mkApp 
-			  ((Lazy.force sig_).intro, 
-			   [| u; p; cx; 
-		  	      mkEvar (key, evar_args ctx) |])))
-	  | None -> 
-	      (try 
-		 let cstrs = Reduction.conv (Global.env ()) x y 
-		 in
-		   ignore(Univ.merge_constraints cstrs (Global.universes ()));
-		   Some (fun x ->
-			   mkCast (x, DEFAULTcast, y))
-	       with 
-		   Reduction.NotConvertible ->	
-		     subtyping_error 
-		       (UncoercibleRewrite (my_print_constr ctx x,
-					    my_print_constr ctx y))
-		 | e -> raise e)
-		
-and rewrite_term prog_info ctx (t : dterm_loc) : Term.constr * Term.types =
-  let rec aux ctx (loc, t) =
-    match t with 
-      | DRel i -> 
-	  let (_, term, typ) = List.nth ctx i in
-	  let t = mkRel (succ i) in
-	    t, Term.lift (succ i) typ
-	  
-      | DLambda ((name, targ), e, t) -> 
-	  let argt, argtt = rewrite_type prog_info ctx targ in
-	  let coqe, et = 
-	    rewrite_term prog_info ((snd name, None, argt) :: ctx) e 
-	  in
-	  let coqt = mkLambda (snd name, argt, coqe) 
-	  and t = mkProd (snd name, argt, et) in
-	    (coqt, t)
-	    
-      | DApp (f, e, t) -> 
-	  let cf, ft = rewrite_term prog_info ctx f in
-	  let coercef, coqt = muterm prog_info ctx ft in
-	  let narg, targ, tres =
-	    match decompose_prod_n 1 coqt with
-		[x, y], z -> x, y, z
-	      | _ -> assert(false)
-	  in
-	  let ce, te = rewrite_term prog_info ctx e in
-	  debug 2 (str "Coercion for application" ++
-		     my_print_constr ctx cf ++ spc () 
-		   ++ my_print_constr ctx ce);
-	  let call x = 
-	    let len = List.length ctx in
-	    let cf = app_opt coercef cf in
-	      match prog_info.rec_info with 
-		  Some r ->
-		    (match kind_of_term cf with
-			 Rel i when i = (pred len) ->
-			   debug 3 (str "Spotted recursive call!");
-			   let ctx', proof = 
-			     subst_ctx ctx (mkApp (r.wf_relation, 
-						   [| x; mkRel len |]))
-			   in 
-			   let evarinfo = 
-			     { 
-			       Evd.evar_concl = proof;
-			       Evd.evar_hyps = 
-			        Environ.val_of_named_context 
-				 (evar_ctx prog_info ctx');
-			       Evd.evar_body = Evd.Evar_empty;
-			     }
-			   in
-			   let key = mknewexist () in
-			     prog_info.evm <- Evd.add prog_info.evm key evarinfo;
-			     mkApp (cf, [| x; mkEvar(key, evar_args ctx) |])
-		       | _ -> mkApp (cf, [| x |]))
-		| None -> mkApp (cf, [| x |])
-	  in
-	  let coercee = coerce prog_info ctx te targ in
-	  let t' = Term.subst1 (app_opt coercee ce) tres in
-	  let t = call (app_opt coercee ce) in
-	    debug 2 (str "Term obtained after coercion (at application): " ++
-		       Termops.print_constr_env (env_of_ctx ctx) t);
-	    t, t'
-	      
-      | DSum ((x, t), (t', u), stype) ->
-	  let ct, ctt = rewrite_term prog_info ctx t in	    
-	  let ctxterm = (snd x, Some ct, ctt) :: ctx in
-	  let ctxtype = (snd x, Some ct, ctt) :: ctx in
-	  let ct', tt' = rewrite_term prog_info ctxterm t' in
-	  let cu, _ = rewrite_type prog_info ctxtype u in
-	  let coercet' = coerce prog_info ctxtype tt' cu in
-	  let lam = Term.subst1 ct (app_opt coercet' ct') in
-	    debug 1 (str "Term obtained after coercion: " ++
-		     Termops.print_constr_env (env_of_ctx ctx) lam);
-	    
-	  let t' = 
-	    mkApp ((Lazy.force existS).typ, 
-		   [| ctt; mkLambda (snd x, ctt, cu) |])
-	  in
-	    mkApp ((Lazy.force existS).intro, 
-		   [| ctt ; mkLambda (snd x, ctt, cu);
-		      ct; lam |]), t'
-	      
-      | DLetIn (x, e, e', t) ->
-	  let ce, et' = rewrite_term prog_info ctx e in
-	  let ce', t' = aux ((snd x, (Some ce), et') :: ctx) e' in
-	    mkLetIn (snd x, ce, et', ce'), t'
-	      
-      | DLetTuple (l, e, e', t) ->
-	  (* let (a, b) = e in e', l = [b, a] *)
-	  let ce, et = rewrite_term prog_info ctx e in
-	    debug 1 (str "Let tuple, e = " ++ 
-		       my_print_constr ctx ce ++
-		       str "type of e: " ++ my_print_constr ctx et);
-	    let l, ctx' = 
-	      let rec aux acc ctx = function
-		  (x, t, t') :: tl ->
-		    let tx, _ = rewrite_type prog_info ctx t in
-		    let trest, _ = rewrite_type prog_info ctx t' in
-		    let ctx' = (snd x, None, tx) :: ctx in
-		      aux ((x, tx, trest) :: acc) ctx' tl
-		| [] -> (acc), ctx
-	      in aux [] ctx (List.rev l)
-	    in
-	      let ce', et' = aux ctx' e' in
-	      let et' = mkLambda (Anonymous, et, 
-				  unlift (pred (List.length l)) et') in
-		debug 1 (str "Let tuple, type of e': " ++
-			   my_print_constr ctx' et');
-
-	  let ind = destInd (Lazy.force existSind) in
-	  let ci = Inductiveops.make_default_case_info 
-	    (Global.env ()) RegularStyle ind 
-	  in
-	  let lambda = 
-	    let rec aux acc = function
-		(x, t, tt) :: (_ :: _) as tl ->
-		  let lam = mkLambda (snd x, t, acc) in
-		  let term = 
-		    mkLambda (make_name "dummy", tt,
-			      mkCase (ci, et', mkRel 1, [| lam |]))
-		  in aux term tl
-	      | (x, t, _) :: [] ->
-		  let lam = mkLambda (snd x, t, acc) in
-		    mkCase (ci, et', ce, [| lam |])
-	      | _ -> assert(false)
-	    in
-	      match l with
-		  (x, t, t') :: tl -> 
-		    aux (mkLambda (snd x, t, ce')) tl
-		| [] -> failwith "DLetTuple with empty list!"
-	  in 
-	    debug 1 (str "Let tuple term: " ++ my_print_constr ctx lambda);
-	    lambda, et'
-	      
-      | DIfThenElse (b, e, e', tif) ->
-	  let name = Name (id_of_string "H") in
-	  let (cb, tb) = aux ctx b in
-	    (match if_branches tb with
-		 Some (ind, (t, f)) ->
-		   let ci = Inductiveops.make_default_case_info 
-		     (Global.env ()) IfStyle ind 
-		   in
-		   let (ce, te), (ce', te') =
-		     aux ((name, None, t) :: ctx) e, 
-		     aux ((name, None, f) :: ctx) e'
-		   in
-		   let lam = mkLambda (Anonymous, tb, te) in
-		   let true_case = 
-		     mkLambda (name, t, ce)
-		   and false_case = 
-		     mkLambda (name, f, ce')
-		   in
-		     (mkCase (ci, lam, cb, [| true_case; false_case |])),
-		       (Termops.pop te)
-	       | None -> failwith ("Ill-typed if"))
-	       
-
-      | DCoq (constr, t) -> constr, 
-	  Typing.type_of (env_of_ctx ctx) prog_info.evm constr	  
-      
-  in aux ctx t
-
-let global_kind = Decl_kinds.IsDefinition Decl_kinds.Definition
-let goal_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Definition
-  
-let make_fixpoint t id term = 
-  let term' = mkLambda (Name id, t.f_fulltype, term) in
-    mkApp (Lazy.force fix, 
-	   [| t.arg_type; t.wf_relation; t.wf_proof; t.f_type; 
-	      mkLambda (Name t.arg_name, t.arg_type, term') |])       
-
-let subtac recursive id (s, t) =
-  check_required_library ["Coq";"Init";"Datatypes"];
-  check_required_library ["Coq";"Init";"Specif"];
-  try
-    let prog_info = { evm = Evd.empty; rec_info = None } in
-    trace (str "Begin infer_type of given spec");
-    let coqtype, coqtype', coqtype'', prog_info, ctx, coqctx =
-      match recursive with
-	  Some (n, t, rel, proof) -> 
-	    let t' = infer_type [] t in
-	    let namen = Name n in
-	    let coqt = infer_type [namen, t'] s in
-	    let t'', _ = rewrite_type prog_info [] t' in
-	    let coqt', _ = rewrite_type prog_info [namen, None, t''] coqt in
-	    let ftype = mkLambda (namen, t'', coqt') in
-	    let fulltype =
-	      mkProd (namen, t'',
-		      mkProd(Anonymous,
-			     mkApp (rel, [| mkRel 1; mkRel 2 |]),
-			     Term.subst1 (mkRel 2) coqt'))
-	    in
-	    let proof = 
-	      match proof with
-		  ManualProof p -> p (* Check that t is a proof of well_founded rel *)
-		| AutoProof ->
-		    (try Lazy.force (Hashtbl.find wf_relations rel)
-		     with Not_found ->
-		       msg_warning
-			 (str "No proof found for relation " 
-			  ++ my_print_constr [] rel);
-		       raise Not_found)
-		| ExistentialProof ->
-		    let wf_rel = mkApp (Lazy.force well_founded, [| t''; rel |]) in
-		    let key = mknewexist () in
-		      prog_info.evm <- Evd.add prog_info.evm key 
-			{ Evd.evar_concl = wf_rel;
-			  Evd.evar_hyps = Environ.empty_named_context_val;
-			  Evd.evar_body = Evd.Evar_empty };
-		      mkEvar (key, [| |])
-	    in
-	    let prog_info = 
-	      let rec_info = 
-		{ arg_name = n;
-		  arg_type = t'';
-		  wf_relation = rel;
-		  wf_proof = proof;
-		  f_type = ftype;
-		  f_fulltype = fulltype;
-		}
-	      in { prog_info with rec_info = Some rec_info }
-	    in
-	    let coqtype = dummy_loc,
-	      DTPi (((dummy_loc, namen), t'), coqt, 
-		    sort_of_dtype_loc [] coqt)
-	    in
-	    let coqtype' = mkProd (namen, t'', coqt') in
-	    let ctx = [(Name id, coqtype); (namen, t')] 
-	    and coqctx = 
-	      [(Name id, None, coqtype'); (namen, None, t'')] 
-	    in coqt, coqt', coqtype', prog_info, ctx, coqctx
-	| None ->
-	    let coqt = infer_type [] s in
-	    let coqt', _ = rewrite_type prog_info [] coqt in
-	      coqt, coqt', coqt', prog_info, [], []
-    in
-    trace (str "Rewrite of coqtype done" ++ 
-	     str "coqtype' = " ++ pr_constr coqtype');
-    let dterm, dtype = infer ctx t in
-    trace (str "Inference done" ++ spc () ++
-	     str "Infered term: " ++ print_dterm_loc ctx dterm ++ spc () ++
-	     str "Infered type: " ++ print_dtype_loc ctx dtype);
-    let dterm', dtype' = 
-      fst (rewrite_term prog_info coqctx dterm),
-      fst (rewrite_type prog_info coqctx dtype)
-    in
-    trace (str "Rewrite done" ++ spc () ++
-	     str "Inferred Coq term:" ++ pr_constr dterm' ++ spc () ++
-	     str "Inferred Coq type:" ++ pr_constr dtype' ++ spc () ++
-	     str "Rewritten Coq type:" ++ pr_constr coqtype');
-    let coercespec = coerce prog_info coqctx dtype' coqtype' in
-    trace (str "Specs coercion successfull");
-    let realt = app_opt coercespec dterm' in
-    trace (str "Term Specs coercion successfull" ++ 
-	     my_print_constr coqctx realt);
-    let realt = 
-      match prog_info.rec_info with
-	  Some t -> make_fixpoint t id realt
-	| None -> realt
-    in
-    trace (str "Coq term" ++ my_print_constr [] realt);
-    trace (str "Coq type" ++ my_print_constr [] coqtype'');
-    let evm = prog_info.evm in
-    (try trace (str "Original evar 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");
-    Command.start_proof id goal_kind coqtype'' (fun _ _ -> ());
-    msgnl (str "Started proof");
-    Pfedit.by tac
-  with 
-    | Typing_error e ->
-	msg_warning (str "Type error in Program tactic:");
-	let cmds = 
-	  (match e with
-	     | NonFunctionalApp (loc, x, mux) ->
-		 str "non functional type app of term " ++ 
-		   x ++ str " of (mu) type " ++ mux
-	     | NonSigma (loc, t) ->
-		 str "Term is not of Sigma type: " ++ t
-	     | NonConvertible (loc, x, y) ->
-		 str "Unconvertible terms:" ++ spc () ++
-		   x ++ spc () ++ str "and" ++ spc () ++ y
-	  )
-	in msg_warning cmds
-	     
-    | Subtyping_error e ->
-	msg_warning (str "(Program tactic) Subtyping error:");
-	let cmds = 
-	  match e with
-	    | UncoercibleInferType (loc, x, y) ->
-		str "Uncoercible terms:" ++ spc ()
-		++ x ++ spc () ++ str "and" ++ spc () ++ y
-	    | UncoercibleInferTerm (loc, x, y, tx, ty) ->
-		str "Uncoercible terms:" ++ spc ()
-		++ tx ++ spc () ++ str "of" ++ spc () ++ str "type" ++ spc () ++ x
-		++ str "and" ++ spc() ++ ty ++ spc () ++ str "of" ++ spc () ++ str "type" ++ spc () ++ y
-	    | UncoercibleRewrite (x, y) ->
-		str "Uncoercible terms:" ++ spc ()
-		++ x ++ spc () ++ str "and" ++ spc () ++ y
-	in msg_warning cmds
-
-    | e -> raise e