Everything compiles again.

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

4 files changed, 277 insertions, 90 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 8652dbd03..ef65f2d8f 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -507,14 +507,15 @@ let occur_in_rhs na rhs =
     | Name id -> List.mem id rhs.rhs_vars
 
 let is_dep_patt_in eqn = function
-  | PatVar (_,name) -> occur_in_rhs name eqn.rhs
+  | PatVar (_,name) -> Flags.is_program_mode () || occur_in_rhs name eqn.rhs
   | PatCstr _ -> true
 
 let mk_dep_patt_row (pats,_,eqn) =
   List.map (is_dep_patt_in eqn) pats
 
 let dependencies_in_pure_rhs nargs eqns =
-  if eqns = [] then list_make nargs false (* Only "_" patts *) else
+  if eqns = [] && not (Flags.is_program_mode ()) then
+    list_make nargs false (* Only "_" patts *) else
   let deps_rows = List.map mk_dep_patt_row eqns in
   let deps_columns = matrix_transpose deps_rows in
   List.map (List.exists ((=) true)) deps_columns
@@ -1321,7 +1322,7 @@ and compile_alias pb (na,orig,(expanded,expanded_typ)) rest =
         else
           mkLetIn (na,c,t,j.uj_val);
       uj_type = subst1 c j.uj_type } in
-  if isRel orig or isVar orig then
+  if not (Flags.is_program_mode ()) && (isRel orig or isVar orig) then
     (* Try to compile first using non expanded alias *)
     try f orig (Retyping.get_type_of pb.env !(pb.evdref) orig)
     with e when precatchable_exception e ->
@@ -1784,7 +1785,7 @@ let prepare_predicate loc typing_fun sigma env tomatchs arsign tycon pred =
       sigma,nal,pred)
     preds
 
-module ProgramCases = struct
+(** Program cases *)
 
 open Program
 
@@ -1833,7 +1834,8 @@ let constr_of_pat env isevars arsign pat avoid =
 	      let previd, id = prime avoid (Name (id_of_string "wildcard")) in
 		Name id, id :: avoid
 	in
-	  PatVar (l, name), [name, None, ty] @ realargs, mkRel 1, ty, (List.map (fun x -> mkRel 1) realargs), 1, avoid
+	  (PatVar (l, name), [name, None, ty] @ realargs, mkRel 1, ty, 
+	   (List.map (fun x -> mkRel 1) realargs), 1, avoid)
     | PatCstr (l,((_, i) as cstr),args,alias) ->
 	let cind = inductive_of_constructor cstr in
 	let IndType (indf, _) = 
@@ -1851,7 +1853,8 @@ let constr_of_pat env isevars arsign pat avoid =
 	  List.fold_right2
 	    (fun (na, c, t) ua (patargs, args, sign, env, n, m, avoid)  ->
 	       let pat', sign', arg', typ', argtypargs, n', avoid =
-		 typ env (substl args (liftn (List.length sign) (succ (List.length args)) t), []) ua avoid
+		 let liftt = liftn (List.length sign) (succ (List.length args)) t in
+		   typ env (substl args liftt, []) ua avoid
 	       in
 	       let args' = arg' :: List.map (lift n') args in
 	       let env' = push_rels sign' env in
@@ -1875,7 +1878,8 @@ let constr_of_pat env isevars arsign pat avoid =
 		let sign, i, avoid =
 		  try
 		    let env = push_rels sign env in
-		    isevars := the_conv_x_leq (push_rels sign env) (lift (succ m) ty) (lift 1 apptype) !isevars;
+		    isevars := the_conv_x_leq (push_rels sign env)
+		      (lift (succ m) ty) (lift 1 apptype) !isevars;
 		    let eq_t = mk_eq (lift (succ m) ty)
 		      (mkRel 1) (* alias *)
 		      (lift 1 app) (* aliased term *)
@@ -1928,7 +1932,8 @@ let rec is_included x y =
 	if i = i' then List.for_all2 is_included args args'
 	else false
 
-(* liftsign is the current pattern's complete signature length. Hence pats is already typed in its
+(* liftsign is the current pattern's complete signature length. 
+   Hence pats is already typed in its
    full signature. However prevpatterns are in the original one signature per pattern form.
  *)
 let build_ineqs prevpatterns pats liftsign =
@@ -1964,13 +1969,13 @@ let build_ineqs prevpatterns pats liftsign =
 	 in match acc with
 	     None -> c
 	   | Some (sign, len, _, c') ->
-	       let conj = it_mkProd_or_LetIn (mk_coq_not (mk_coq_conj c'))
+	       let conj = it_mkProd_or_LetIn (mk_coq_not (mk_coq_and c'))
 		 (lift_rel_context liftsign sign)
 	       in
 		 conj :: c)
       [] prevpatterns
   in match diffs with [] -> None
-    | _ -> Some (mk_coq_conj diffs)
+    | _ -> Some (mk_coq_and diffs)
 
 let subst_rel_context k ctx subst =
   let (_, ctx') =
@@ -2009,14 +2014,16 @@ let constrs_of_pats typing_fun env isevars eqns tomatchs sign neqs arity =
 	       let len = List.length sign' in
 		 (sign' @ renv,
 		 (* lift to get outside of previous pattern's signatures. *)
-		 (sign', liftn n (succ len) c, (s, List.map (liftn n (succ len)) args), p) :: pats,
+		 (sign', liftn n (succ len) c, 
+		  (s, List.map (liftn n (succ len)) args), p) :: pats,
 		 len + n))
 	     ([], [], 0) opats in
 	 let pats, _ = List.fold_left
 	   (* lift to get outside of past patterns to get terms in the combined environment. *)
 	   (fun (pats, n) (sign, c, (s, args), p) ->
 	     let len = List.length sign in
-	       ((rels_of_patsign sign, lift n c, (s, List.map (lift n) args), p) :: pats, len + n))
+	       ((rels_of_patsign sign, lift n c,
+		 (s, List.map (lift n) args), p) :: pats, len + n))
 	   ([], 0) pats
 	 in
 	 let ineqs = build_ineqs prevpatterns pats signlen in
@@ -2077,7 +2084,9 @@ let constrs_of_pats typing_fun env isevars eqns tomatchs sign neqs arity =
 
 let lift_ctx n ctx =
   let ctx', _ =
-    List.fold_right (fun (c, t) (ctx, n') -> (liftn n n' c, liftn_tomatch_type n n' t) :: ctx, succ n') ctx ([], 0)
+    List.fold_right (fun (c, t) (ctx, n') -> 
+		       (liftn n n' c, liftn_tomatch_type n n' t) :: ctx, succ n') 
+      ctx ([], 0)
   in ctx'
 
 (* Turn matched terms into variables. *)
@@ -2117,70 +2126,70 @@ let build_dependent_signature env evars avoid tomatchs arsign =
 	    new arity signatures
 	 *)
 	 match ty with
-	     IsInd (ty, IndType (indf, args), _) when List.length args > 0 ->
-	       (* Build the arity signature following the names in matched terms as much as possible *)
-	       let argsign = List.tl arsign in (* arguments in inverse application order *)
-	       let (appn, appb, appt) as _appsign = List.hd arsign in (* The matched argument *)
-	       let argsign = List.rev argsign in (* arguments in application order *)
-	       let env', nargeqs, argeqs, refl_args, slift, argsign' =
-		 List.fold_left2
-		   (fun (env, nargeqs, argeqs, refl_args, slift, argsign') arg (name, b, t) ->
-		      let argt = Retyping.get_type_of env evars arg in
-		      let eq, refl_arg =
-			if Reductionops.is_conv env evars argt t then
-			  (mk_eq (lift (nargeqs + slift) argt)
-			     (mkRel (nargeqs + slift))
-			     (lift (nargeqs + nar) arg),
-			   mk_eq_refl argt arg)
-			else
-			  (mk_JMeq (lift (nargeqs + slift) t)
-			     (mkRel (nargeqs + slift))
-			     (lift (nargeqs + nar) argt)
-			     (lift (nargeqs + nar) arg),
-			   mk_JMeq_refl argt arg)
-		      in
-		      let previd, id =
-			let name =
-			  match kind_of_term arg with
-			      Rel n -> pi1 (lookup_rel n env)
-			    | _ -> name
-			in
-			  make_prime avoid name
+	 | IsInd (ty, IndType (indf, args), _) when List.length args > 0 ->
+	     (* Build the arity signature following the names in matched terms 
+		as much as possible *)
+	     let argsign = List.tl arsign in (* arguments in inverse application order *)
+	     let (appn, appb, appt) as _appsign = List.hd arsign in (* The matched argument *)
+	     let argsign = List.rev argsign in (* arguments in application order *)
+	     let env', nargeqs, argeqs, refl_args, slift, argsign' =
+	       List.fold_left2
+		 (fun (env, nargeqs, argeqs, refl_args, slift, argsign') arg (name, b, t) ->
+		    let argt = Retyping.get_type_of env evars arg in
+		    let eq, refl_arg =
+		      if Reductionops.is_conv env evars argt t then
+			(mk_eq (lift (nargeqs + slift) argt)
+			   (mkRel (nargeqs + slift))
+			   (lift (nargeqs + nar) arg),
+			 mk_eq_refl argt arg)
+		      else
+			(mk_JMeq (lift (nargeqs + slift) t)
+			   (mkRel (nargeqs + slift))
+			   (lift (nargeqs + nar) argt)
+			   (lift (nargeqs + nar) arg),
+			 mk_JMeq_refl argt arg)
+		    in
+		    let previd, id =
+		      let name =
+			match kind_of_term arg with
+			Rel n -> pi1 (lookup_rel n env)
+			| _ -> name
 		      in
-			(env, succ nargeqs,
-			 (Name (eq_id avoid previd), None, eq) :: argeqs,
-			 refl_arg :: refl_args,
-			 pred slift,
-			 (Name id, b, t) :: argsign'))
-		   (env, neqs, [], [], slift, []) args argsign
-	       in
-	       let eq = mk_JMeq
-		 (lift (nargeqs + slift) appt)
-		 (mkRel (nargeqs + slift))
-		 (lift (nargeqs + nar) ty)
-		 (lift (nargeqs + nar) tm)
-	       in
-	       let refl_eq = mk_JMeq_refl ty tm in
-	       let previd, id = make_prime avoid appn in
-		 (((Name (eq_id avoid previd), None, eq) :: argeqs) :: eqs,
-		 succ nargeqs,
-		 refl_eq :: refl_args,
-		 pred slift,
-		 (((Name id, appb, appt) :: argsign') :: arsigns))
-
-	   | _ ->
-	       (* Non dependent inductive or not inductive, just use a regular equality *)
-	       let (name, b, typ) = match arsign with [x] -> x | _ -> assert(false) in
-	       let previd, id = make_prime avoid name in
-	       let arsign' = (Name id, b, typ) in
-	       let tomatch_ty = type_of_tomatch ty in
-	       let eq =
-		 mk_eq (lift nar tomatch_ty)
-		   (mkRel slift) (lift nar tm)
-	       in
-		 ([(Name (eq_id avoid previd), None, eq)] :: eqs, succ neqs,
-		  (mk_eq_refl tomatch_ty tm) :: refl_args,
-		  pred slift, (arsign' :: []) :: arsigns))
+			make_prime avoid name
+		    in
+		      (env, succ nargeqs,
+		       (Name (eq_id avoid previd), None, eq) :: argeqs,
+		       refl_arg :: refl_args,
+		       pred slift,
+		       (Name id, b, t) :: argsign'))
+		 (env, neqs, [], [], slift, []) args argsign
+	     in
+	     let eq = mk_JMeq
+	       (lift (nargeqs + slift) appt)
+	       (mkRel (nargeqs + slift))
+	       (lift (nargeqs + nar) ty)
+	       (lift (nargeqs + nar) tm)
+	     in
+	     let refl_eq = mk_JMeq_refl ty tm in
+	     let previd, id = make_prime avoid appn in
+	       (((Name (eq_id avoid previd), None, eq) :: argeqs) :: eqs,
+		succ nargeqs,
+		refl_eq :: refl_args,
+		pred slift,
+		(((Name id, appb, appt) :: argsign') :: arsigns))
+
+	 | _ -> (* Non dependent inductive or not inductive, just use a regular equality *)
+	     let (name, b, typ) = match arsign with [x] -> x | _ -> assert(false) in
+	     let previd, id = make_prime avoid name in
+	     let arsign' = (Name id, b, typ) in
+	     let tomatch_ty = type_of_tomatch ty in
+	     let eq =
+	       mk_eq (lift nar tomatch_ty)
+		 (mkRel slift) (lift nar tm)
+	     in
+	       ([(Name (eq_id avoid previd), None, eq)] :: eqs, succ neqs,
+		(mk_eq_refl tomatch_ty tm) :: refl_args,
+		pred slift, (arsign' :: []) :: arsigns))
       ([], 0, [], nar, []) tomatchs arsign
   in
   let arsign'' = List.rev arsign' in
@@ -2190,11 +2199,12 @@ let build_dependent_signature env evars avoid tomatchs arsign =
 let context_of_arsign l =
   let (x, _) = List.fold_right
     (fun c (x, n) ->
-      (lift_rel_context n c @ x, List.length c + n))
+       (lift_rel_context n c @ x, List.length c + n))
     l ([], 0)
   in x
 
-let compile_program_cases loc style (typing_function, evdref) tycon env (predopt, tomatchl, eqns) =
+let compile_program_cases loc style (typing_function, evdref) tycon env
+    (predopt, tomatchl, eqns) =
   let typing_fun tycon env = function
     | Some t ->	typing_function tycon env evdref t
     | None -> coq_unit_judge () in
@@ -2253,15 +2263,34 @@ let compile_program_cases loc style (typing_function, evdref) tycon env (predopt
 
   (* We push the initial terms to match and push their alias to rhs' envs *)
   (* names of aliases will be recovered from patterns (hence Anonymous here) *)
-  let initial_pushed = List.map (fun tm -> Pushed (tm,[],Anonymous)) tomatchs in
 
+  let out_tmt na = function NotInd (c,t) -> (na,c,t) | IsInd (typ,_,_) -> (na,None,typ) in
+  let typs = List.map2 (fun na (tm,tmt) -> (tm,out_tmt na tmt)) nal tomatchs in
+    
+  let typs =
+    List.map (fun (c,d) -> (c,extract_inductive_data env !evdref d,d)) typs in
+    
+  let dep_sign =
+    find_dependencies_signature
+      (list_make (List.length typs) true)
+      typs in
+    
+  let typs' =
+    list_map3
+      (fun (tm,tmt) deps na ->
+         let deps = if not (isRel tm) then [] else deps in
+           ((tm,tmt),deps,na))
+      tomatchs dep_sign nal in
+    
+  let initial_pushed = List.map (fun x -> Pushed x) typs' in
+    
   let typing_function tycon env evdref = function
     | Some t ->	typing_function tycon env evdref t
     | None -> coq_unit_judge () in
 
   let pb =
     { env      = env;
-      evdref  = evdref;
+      evdref   = evdref;
       pred     = pred;
       tomatch  = initial_pushed;
       history  = start_history (List.length initial_pushed);
@@ -2278,14 +2307,13 @@ let compile_program_cases loc style (typing_function, evdref) tycon env (predopt
       { uj_val = it_mkLambda_or_LetIn body tomatchs_lets;
 	uj_type = nf_evar !evdref tycon; }
     in j
-end
 
 (**************************************************************************)
 (* Main entry of the matching compilation                                 *)
 
 let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, eqns) =
   if predopt = None && Flags.is_program_mode () then
-    ProgramCases.compile_program_cases loc style (typing_fun, evdref) 
+    compile_program_cases loc style (typing_fun, evdref) 
       tycon env (predopt, tomatchl, eqns)
   else
       
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 39677f38b..d0dd870de 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -55,3 +55,65 @@ val compile_cases :
   env -> glob_constr option * tomatch_tuples * cases_clauses ->
   unsafe_judgment
 
+val constr_of_pat : 
+           Environ.env ->
+           Evd.evar_map ref ->
+           Term.rel_declaration list ->
+           Glob_term.cases_pattern ->
+           Names.identifier list ->
+           Glob_term.cases_pattern *
+           (Term.rel_declaration list * Term.constr *
+            (Term.types * Term.constr list) * Glob_term.cases_pattern) *
+           Names.identifier list
+
+type 'a rhs =
+    { rhs_env    : env;
+      rhs_vars   : identifier list;
+      avoid_ids  : identifier list;
+      it         : 'a option}
+
+type 'a equation =
+    { patterns     : cases_pattern list;
+      rhs          : 'a rhs;
+      alias_stack  : name list;
+      eqn_loc      : loc;
+      used         : bool ref }
+
+type 'a matrix = 'a equation list
+
+(* 1st argument of IsInd is the original ind before extracting the summary *)
+type tomatch_type =
+  | IsInd of types * inductive_type * name list
+  | NotInd of constr option * types
+
+type tomatch_status =
+  | Pushed of ((constr * tomatch_type) * int list * name)
+  | Alias of (name * constr * (constr * types))
+  | NonDepAlias
+  | Abstract of int * rel_declaration
+
+type tomatch_stack = tomatch_status list
+
+(* We keep a constr for aliases and a cases_pattern for error message *)
+
+type pattern_history =
+  | Top
+  | MakeConstructor of constructor * pattern_continuation
+
+and pattern_continuation =
+  | Continuation of int * cases_pattern list * pattern_history
+  | Result of cases_pattern list
+
+type 'a pattern_matching_problem =
+    { env       : env;
+      evdref    : evar_map ref;
+      pred      : constr;
+      tomatch   : tomatch_stack;
+      history   : pattern_continuation;
+      mat       : 'a matrix;
+      caseloc   : loc;
+      casestyle : case_style;
+      typing_function: type_constraint -> env -> evar_map ref -> 'a option -> unsafe_judgment }
+
+
+val compile : 'a pattern_matching_problem -> Environ.unsafe_judgment
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index e75dfcca8..2bbadfded 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -315,6 +315,15 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function
       let ftys = array_map2 (fun e a -> it_mkProd_or_LetIn a e) ctxtv lara in
       let nbfix = Array.length lar in
       let names = Array.map (fun id -> Name id) names in
+      let _ = 
+	match tycon with
+	| Some t -> 
+ 	    let fixi = match fixkind with
+	      | GFix (vn,i) -> i
+	      | GCoFix i -> i
+	    in e_conv env evdref ftys.(fixi) t
+	| None -> true
+      in
 	(* Note: bodies are not used by push_rec_types, so [||] is safe *)
       let newenv = push_rec_types (names,ftys,[||]) env in
       let vdefj =
@@ -341,11 +350,12 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function
 		 but doing it properly involves delta-reduction, and it finally
                  doesn't seem worth the effort (except for huge mutual
 		 fixpoints ?) *)
-	      let possible_indexes = Array.to_list (Array.mapi
-						      (fun i (n,_) -> match n with
-						       | Some n -> [n]
-						       | None -> list_map_i (fun i _ -> i) 0 ctxtv.(i))
-						      vn)
+	      let possible_indexes =
+		Array.to_list (Array.mapi
+				 (fun i (n,_) -> match n with
+				  | Some n -> [n]
+				  | None -> list_map_i (fun i _ -> i) 0 ctxtv.(i))
+				 vn)
 	      in
 	      let fixdecls = (names,ftys,fdefs) in
 	      let indexes = search_guard loc env possible_indexes fixdecls in
@@ -489,10 +499,12 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function
       in
       let cstrs = get_constructors env indf in
 	if Array.length cstrs <> 1 then
-          user_err_loc (loc,"",str "Destructing let is only for inductive types with one constructor.");
+          user_err_loc (loc,"",str "Destructing let is only for inductive types" ++
+			str " with one constructor.");
 	let cs = cstrs.(0) in
 	  if List.length nal <> cs.cs_nargs then
-            user_err_loc (loc,"", str "Destructing let on this type expects " ++ int cs.cs_nargs ++ str " variables.");
+            user_err_loc (loc,"", str "Destructing let on this type expects " ++ 
+			    int cs.cs_nargs ++ str " variables.");
 	  let fsign = List.map2 (fun na (_,c,t) -> (na,c,t))
             (List.rev nal) cs.cs_args in
 	  let env_f = push_rels fsign env in
@@ -636,7 +648,8 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function
 		      with Reduction.NotConvertible -> 
 			error_actual_type_loc loc env !evdref cj tval 
 		    end
-                  else user_err_loc (loc,"",str "Cannot check cast with vm: unresolved arguments remain.")
+                  else user_err_loc (loc,"",str "Cannot check cast with vm: " ++
+				       str "unresolved arguments remain.")
 	      | _ -> inh_conv_coerce_to_tycon loc env evdref cj (mk_tycon tval)
 	    in
 	    let v = mkCast (cj.uj_val, k, tval) in
diff --git a/pretyping/program.ml b/pretyping/program.ml
new file mode 100644
index 000000000..bb0cbe1c7
--- /dev/null
+++ b/pretyping/program.ml
@@ -0,0 +1,84 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open Errors
+open Util
+open Names
+open Term
+open Reductionops
+open Environ
+open Typeops
+open Pretype_errors
+open Classops
+open Recordops
+open Evarutil
+open Evarconv
+open Retyping
+open Evd
+open Termops
+
+type message = string
+
+let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
+
+let find_reference locstr dir s =
+  let sp = Libnames.make_path (make_dir dir) (id_of_string s) in
+  try Nametab.global_of_path sp
+  with Not_found -> anomaly (locstr^": cannot find "^(Libnames.string_of_path sp))
+
+let coq_reference locstr dir s = find_reference locstr ("Coq"::dir) s
+let coq_constant locstr dir s = Libnames.constr_of_global (coq_reference locstr dir s)
+
+let init_constant dir s () = coq_constant "Program" dir s
+let init_reference dir s () = coq_reference "Program" dir s
+
+let sig_typ = init_constant ["Init"; "Specif"] "sig"
+let sig_intro = init_constant ["Init"; "Specif"] "exist"
+let sig_proj1 = init_constant ["Init"; "Specif"] "proj1_sig"
+
+let sigT_typ = init_constant ["Init"; "Specif"] "sigT"
+let sigT_intro = init_constant ["Init"; "Specif"] "existT"
+let sigT_proj1 = init_constant ["Init"; "Specif"] "projT1"
+let sigT_proj2 = init_constant ["Init"; "Specif"] "projT2"
+
+let prod_typ = init_constant ["Init"; "Datatypes"] "prod"
+let prod_intro = init_constant ["Init"; "Datatypes"] "pair"
+let prod_proj1 = init_constant ["Init"; "Datatypes"] "fst"
+let prod_proj2 = init_constant ["Init"; "Datatypes"] "snd"
+
+let coq_eq_ind = init_constant ["Init"; "Logic"] "eq"
+let coq_eq_refl = init_constant ["Init"; "Logic"] "eq_refl"
+let coq_eq_refl_ref = init_reference ["Init"; "Logic"] "eq_refl"
+let coq_eq_rect = init_constant ["Init"; "Logic"] "eq_rect"
+
+let coq_JMeq_ind = init_constant ["Logic";"JMeq"] "JMeq"
+let coq_JMeq_refl = init_constant ["Logic";"JMeq"] "JMeq_refl"
+
+let coq_not = init_constant ["Init";"Logic"] "not"
+let coq_and = init_constant ["Init";"Logic"] "and"
+
+let mk_coq_not x = mkApp (delayed_force coq_not, [| x |])
+
+let unsafe_fold_right f = function
+    hd :: tl -> List.fold_right f tl hd
+  | [] -> raise (Invalid_argument "unsafe_fold_right")
+
+let mk_coq_and l =
+  let and_typ = delayed_force coq_and in
+    unsafe_fold_right
+      (fun c conj ->
+	 mkApp (and_typ, [| c ; conj |]))
+      l
+
+let with_program f c = 
+  let mode = !Flags.program_mode in
+    Flags.program_mode := true;
+    let res = f c in
+      Flags.program_mode := mode;
+      res