modifs pour premiere edition de liens

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

11 files changed, 479 insertions, 25 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
new file mode 100644
index 0000000000..6abd8d6acd
--- /dev/null
+++ b/pretyping/cases.ml
@@ -0,0 +1,5 @@
+
+(* $Id$ *)
+
+let compile_multcase _ _ _ = failwith "compile_multcase: TODO"
+
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index 41b3cff696..c510299acf 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -19,10 +19,10 @@ val inh_tosort :
   env -> 'a evar_defs -> unsafe_judgment -> unsafe_judgment
 val inh_ass_of_j : env -> 'a evar_defs ->
   unsafe_judgment -> typed_type
-val inh_coerce_to : env -> unit evar_defs ->
+val inh_coerce_to : env -> 'a evar_defs ->
   constr -> unsafe_judgment -> unsafe_judgment
-val inh_cast_rel : env -> unit evar_defs ->
+val inh_cast_rel : env -> 'a evar_defs ->
   unsafe_judgment -> unsafe_judgment -> unsafe_judgment
-val inh_apply_rel_list : bool -> env -> unit evar_defs ->
+val inh_apply_rel_list : bool -> env -> 'a evar_defs ->
   unsafe_judgment list -> unsafe_judgment -> 'b * ('c * constr option) 
     -> unsafe_judgment
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 9310e5dd38..972109d2f1 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -11,18 +11,18 @@ open Evarutil
 
 val reset_problems : unit -> unit
 
-val the_conv_x : env -> unit evar_defs -> constr -> constr -> bool
+val the_conv_x : env -> 'a evar_defs -> constr -> constr -> bool
 
-val the_conv_x_leq : env -> unit evar_defs -> constr -> constr -> bool
+val the_conv_x_leq : env -> 'a evar_defs -> constr -> constr -> bool
 
 (* For debugging *)
 val solve_pb : 
-  env -> unit evar_defs -> conv_pb * constr * constr -> bool
+  env -> 'a evar_defs -> conv_pb * constr * constr -> bool
 
 val evar_conv_x : 
-  env -> unit evar_defs ->
+  env -> 'a evar_defs ->
     conv_pb -> constr -> constr -> bool
 
 val evar_eqappr_x : 
-  env -> unit evar_defs ->
+  env -> 'a evar_defs ->
     conv_pb -> constr * constr list -> constr * constr list -> bool
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 226b6ff0de..c1313ee142 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -50,7 +50,7 @@ let new_isevar_sign env sigma typ args =
     error "new_isevar_sign: two vars have the same name";
   let newev = Evd.new_evar() in
   let info = { evar_concl = typ; evar_env = env; 
-	       evar_body = Evar_empty; evar_info = () } in
+	       evar_body = Evar_empty; evar_info = None } in
   (Evd.add sigma newev info, mkEvar newev args)
 
 (* We don't try to guess in which sort the type should be defined, since
@@ -278,7 +278,7 @@ let solve_refl conv_algo isevars c1 c2 =
   let nargs = (Array.of_list (List.map mkVar (ids_of_sign nsign))) in
   let newev = Evd.new_evar () in
   let info = { evar_concl = evd.evar_concl; evar_env = nenv;
-	       evar_body = Evar_empty; evar_info = () } in
+	       evar_body = Evar_empty; evar_info = None } in
   isevars :=
     Evd.define (Evd.add !isevars newev info) ev (mkEvar newev nargs);
   Some [ev]
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 501e9f28ec..21f4897815 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -22,7 +22,7 @@ val filter_sign :
   'a * identifier list * var_context
 
 val dummy_sort : constr
-val do_restrict_hyps : unit evar_map -> constr -> unit evar_map * constr
+val do_restrict_hyps : 'a evar_map -> constr -> 'a evar_map * constr
 
 
 type 'a evar_defs = 'a evar_map ref
@@ -33,11 +33,11 @@ val ise_undefined : 'a evar_defs -> constr -> bool
 val ise_defined : 'a evar_defs -> constr -> bool
 
 val real_clean :
-  unit evar_defs -> int -> (identifier * constr) list -> constr -> constr
+  'a evar_defs -> int -> (identifier * constr) list -> constr -> constr
 val new_isevar :
-  unit evar_defs -> env -> constr -> path_kind -> constr * constr
-val evar_define : unit evar_defs -> constr -> constr -> int list
-val solve_simple_eqn : (constr -> constr -> bool) -> unit evar_defs ->
+  'a evar_defs -> env -> constr -> path_kind -> constr * constr
+val evar_define : 'a evar_defs -> constr -> constr -> int list
+val solve_simple_eqn : (constr -> constr -> bool) -> 'a evar_defs ->
   (conv_pb * constr * constr) -> int list option
 
 val has_undefined_isevars : 'a evar_defs -> constr -> bool
@@ -59,13 +59,13 @@ val mk_tycon2 : trad_constraint -> constr -> trad_constraint
 
 (* application *)
 val app_dom_tycon : 
-  env -> unit evar_defs -> trad_constraint -> trad_constraint
+  env -> 'a evar_defs -> trad_constraint -> trad_constraint
 val app_rng_tycon :
   env -> 'a evar_defs -> constr -> trad_constraint -> trad_constraint
 
 (* abstraction *)
 val abs_dom_valcon : 
-  env -> unit evar_defs -> trad_constraint -> trad_constraint
+  env -> 'a evar_defs -> trad_constraint -> trad_constraint
 val abs_rng_tycon : 
   env -> 'a evar_defs -> trad_constraint -> trad_constraint
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 96e97a040d..05d73ffa1b 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -213,7 +213,7 @@ let pretype_ref loc isevars env = function
     let metaty =
       try List.assoc n !trad_metamap
       with Not_found ->
-	Ast.user_err_loc 
+	user_err_loc 
 	  (loc,"pretype",
 	   [< 'sTR "Metavariable "; 'iNT n; 'sTR "remains non instanciated" >])
 	  in
@@ -297,7 +297,7 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
       (match loc with
 	  None -> anomaly "There is an implicit argument I cannot solve"
 	| Some loc -> 
-	    Ast.user_err_loc
+	    user_err_loc
 	      (loc,"pretype",
 	       [< 'sTR "Cannot infer a term for this placeholder" >]))
   | _ -> anomaly "tycon")
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index c22653dab4..97ace7b8ab 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -40,22 +40,22 @@ i*)
 
 (* Raw calls to the inference machine of Trad: boolean says if we must fail
  * on unresolved evars, or replace them by Metas *)
-val ise_resolve : bool -> unit evar_map -> (int * constr) list ->
+val ise_resolve : bool -> 'a evar_map -> (int * constr) list ->
   env -> rawconstr -> unsafe_judgment
-val ise_resolve_type : bool -> unit evar_map -> (int * constr) list ->
+val ise_resolve_type : bool -> 'a evar_map -> (int * constr) list ->
   env -> rawconstr -> typed_type
 
 (* Call [ise_resolve] with empty metamap and [fail_evar=true]. The boolean says
  * if we must coerce to a type *)
-val ise_resolve1 : bool -> unit evar_map -> env -> rawconstr -> constr
+val ise_resolve1 : bool -> 'a evar_map -> env -> rawconstr -> constr
 
-val ise_resolve_casted : unit evar_map -> env -> 
+val ise_resolve_casted : 'a evar_map -> env -> 
   constr -> rawconstr -> constr
 
 (* progmach.ml tries to type ill-typed terms: does not perform the conversion
  * test in application.
  *)
-val ise_resolve_nocheck : unit evar_map -> (int * constr) list ->
+val ise_resolve_nocheck : 'a evar_map -> (int * constr) list ->
   env -> rawconstr -> unsafe_judgment
 
 
@@ -63,5 +63,5 @@ val ise_resolve_nocheck : unit evar_map -> (int * constr) list ->
  * Unused outside Trad, but useful for debugging
  *)
 val pretype : 
-  trad_constraint -> env -> unit evar_defs -> rawconstr 
+  trad_constraint -> env -> 'a evar_defs -> rawconstr 
     -> unsafe_judgment
diff --git a/pretyping/syntax_def.ml b/pretyping/syntax_def.ml
new file mode 100644
index 0000000000..85f6344057
--- /dev/null
+++ b/pretyping/syntax_def.ml
@@ -0,0 +1,43 @@
+
+(* $Id$ *)
+
+open Names
+open Rawterm
+open Libobject
+open Lib
+
+(* Syntactic definitions. *)
+
+let syntax_table = ref (Idmap.empty : rawconstr Idmap.t)
+
+let _ = Summary.declare_summary
+	  "SYNTAXCONSTANT"
+	  { Summary.freeze_function = (fun () -> !syntax_table);
+	    Summary.unfreeze_function = (fun ft -> syntax_table := ft);
+	    Summary.init_function = (fun () -> syntax_table := Idmap.empty) }
+
+let add_syntax_constant id c =
+  syntax_table := Idmap.add id c !syntax_table
+
+let cache_syntax_constant (sp,c) = 
+  add_syntax_constant (basename sp) c;
+  Nametab.push (basename sp) sp
+
+let open_syntax_constant (sp,_) =
+  Nametab.push (basename sp) sp
+
+let (in_syntax_constant, out_syntax_constant) =
+  let od = {
+    cache_function = cache_syntax_constant;
+    load_function = (fun _ -> ());
+    open_function = open_syntax_constant;
+    specification_function = (fun x -> x) } in
+  declare_object ("SYNTAXCONSTANT", od)
+
+let declare_syntactic_definition id c =
+  let sp = add_leaf id CCI (in_syntax_constant c) in
+  add_syntax_constant id c;
+  Nametab.push (basename sp) sp
+
+let search_syntactic_definition id = Idmap.find id !syntax_table
+
diff --git a/pretyping/syntax_def.mli b/pretyping/syntax_def.mli
new file mode 100644
index 0000000000..f889f24731
--- /dev/null
+++ b/pretyping/syntax_def.mli
@@ -0,0 +1,15 @@
+
+(* $Id$ *)
+
+(*i*)
+open Names
+open Rawterm
+(*i*)
+
+(* Syntactic definitions. *)
+
+val declare_syntactic_definition : identifier -> rawconstr -> unit
+
+val search_syntactic_definition : identifier -> rawconstr
+
+
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
new file mode 100644
index 0000000000..16ea6c5896
--- /dev/null
+++ b/pretyping/tacred.ml
@@ -0,0 +1,353 @@
+
+(* $Id$ *)
+
+open Pp
+open Util
+open Names
+open Generic
+open Term
+open Inductive
+open Environ
+open Reduction
+open Instantiate
+open Redinfo
+
+exception Elimconst
+exception Redelimination
+
+let is_elim c =
+  let (sp, _) = destConst c in
+  match constant_eval sp with
+    | NotAnElimination -> raise Elimconst
+    | Elimination (lv,n,b) -> (lv,n,b)
+
+let rev_firstn_liftn fn ln = 
+  let rec rfprec p res l = 
+    if p = 0 then 
+      res 
+    else
+      match l with
+        | [] -> invalid_arg "Reduction.rev_firstn_liftn"
+        | a::rest -> rfprec (p-1) ((lift ln a)::res) rest
+  in 
+  rfprec fn []
+
+let make_elim_fun f largs =
+  try 
+    let (lv,n,b) = is_elim f 
+    and ll = List.length largs in 
+    if ll < n then raise Redelimination;
+    if b then
+      let labs,_ = list_chop n largs in
+      let p = List.length lv in
+      let la' = list_map_i 
+		  (fun q aq ->
+		     try (Rel (p+1-(list_index (n+1-q) (List.map fst lv)))) 
+		     with Failure _ -> aq) 1
+                  (List.map (lift p) labs) 
+      in
+      list_fold_left_i 
+	(fun i c (k,a) -> 
+           DOP2(Lambda,(substl (rev_firstn_liftn (n-k) (-i) la') a),
+                DLAM(Name(id_of_string"x"),c))) 0 (applistc f la') lv
+    else 
+      f
+  with Elimconst | Failure _ -> 
+    raise Redelimination
+
+let mind_nparams env i =
+  let mis = lookup_mind_specif i env in mis.mis_mib.mind_nparams
+
+(* F is convertible to DOPN(Fix(recindices,bodynum),bodyvect) make 
+   the reduction using this extra information *)
+
+let contract_fix_use_function f fix =
+  match fix with 
+    | DOPN(Fix(recindices,bodynum),bodyvect) ->
+  	let nbodies = Array.length recindices in
+  	let make_Fi j = DOPN(Fix(recindices,j),bodyvect) in
+  	let lbodies = list_assign (list_tabulate make_Fi nbodies) bodynum f in
+	  sAPPViList bodynum (array_last bodyvect) lbodies
+    | _ -> assert false
+
+let reduce_fix_use_function f whfun fix stack =
+  match fix with 
+    | DOPN (Fix(recindices,bodynum),bodyvect) ->
+	(match fix_recarg fix stack with
+           | None -> (false,(fix,stack))
+	   | Some (recargnum,recarg) ->
+               let (recarg'hd,_ as recarg')= whfun recarg [] in
+               let stack' = list_assign stack recargnum (applist recarg') in
+	       (match recarg'hd with
+                  | DOPN(MutConstruct _,_) ->
+		      (true,(contract_fix_use_function f fix,stack'))
+		  | _ -> (false,(fix,stack'))))
+    | _ -> assert false
+
+let contract_cofix_use_function f cofix =
+  match cofix with 
+    | DOPN(CoFix(bodynum),bodyvect) ->
+  	let nbodies =  (Array.length bodyvect) -1 in
+  	let make_Fi j = DOPN(CoFix(j),bodyvect) in
+  	let lbodies = list_assign (list_tabulate make_Fi nbodies) bodynum f in
+  	sAPPViList bodynum (array_last bodyvect) lbodies
+    | _ -> assert false
+
+let reduce_mind_case_use_function env f mia =
+  match mia.mconstr with 
+    | DOPN(MutConstruct((indsp,tyindx),i),_) ->
+	let ind = DOPN(MutInd(indsp,tyindx),args_of_mconstr mia.mconstr) in
+	let nparams = mind_nparams env ind in
+	let real_cargs = snd(list_chop nparams mia.mcargs) in
+	applist (mia.mlf.(i-1),real_cargs)
+    | DOPN(CoFix _,_) as cofix ->
+	let cofix_def = contract_cofix_use_function f cofix in
+	mkMutCaseA mia.mci mia.mP (applist(cofix_def,mia.mcargs)) mia.mlf
+    | _ -> assert false
+	  
+let special_red_case env whfun p c ci lf  =
+  let rec redrec c l = 
+    let (constr,cargs) = whfun c l in 
+    match constr with 
+      | DOPN(Const _,_) as g -> 
+          if evaluable_constant env g then
+            let gvalue = constant_value env g in
+            if reducible_mind_case gvalue then
+              reduce_mind_case_use_function env g
+                {mP=p; mconstr=gvalue; mcargs=cargs; mci=ci; mlf=lf}
+            else 
+	      redrec gvalue cargs
+          else 
+	    raise Redelimination
+      | _ ->
+          if reducible_mind_case constr then
+            reduce_mind_case env
+              {mP=p; mconstr=constr; mcargs=cargs; mci=ci; mlf=lf}
+          else 
+	    raise Redelimination
+  in 
+  redrec c []
+
+let rec red_elim_const env sigma k largs =
+  if not (evaluable_constant env k) then raise Redelimination;
+  let f = make_elim_fun k largs in
+  match whd_betadeltaeta_stack env sigma (constant_value env k) largs with
+    | (DOPN(MutCase _,_) as mc,lrest) ->
+        let (ci,p,c,lf) = destCase mc in
+        (special_red_case env (construct_const env sigma) p c ci lf, lrest)
+    | (DOPN(Fix _,_) as fix,lrest) -> 
+        let (b,(c,rest)) = 
+	  reduce_fix_use_function f (construct_const env sigma) fix lrest
+        in 
+	if b then (nf_beta env sigma c, rest) else raise Redelimination
+    | _ -> assert false
+
+and construct_const env sigma c stack = 
+  let rec hnfstack x stack =
+    match x with
+      | (DOPN(Const _,_)) as k  ->
+          (try
+             let (c',lrest) = red_elim_const env sigma k stack in 
+	     hnfstack c' lrest
+           with Redelimination ->
+             if evaluable_constant env k then 
+	       let cval = constant_value env k in
+	       (match cval with
+                  | DOPN (CoFix _,_) -> (k,stack)
+                  | _ -> hnfstack cval stack) 
+             else 
+	       raise Redelimination)
+      | (DOPN(Abst _,_) as a) ->
+          if evaluable_abst env a then 
+	    hnfstack (abst_value env a) stack
+          else 
+	    raise Redelimination
+      | DOP2(Cast,c,_) -> hnfstack c stack
+      | DOPN(AppL,cl) -> hnfstack (array_hd cl) (array_app_tl cl stack)
+      | DOP2(Lambda,_,DLAM(_,c)) ->
+          (match stack with 
+             | [] -> assert false
+             | c'::rest -> stacklam hnfstack [c'] c rest)
+      | DOPN(MutCase _,_) as c_0 ->
+          let (ci,p,c,lf) = destCase c_0 in
+          hnfstack 
+	    (special_red_case env (construct_const env sigma) p c ci lf) 
+	    stack
+      | DOPN(MutConstruct _,_) as c_0 -> c_0,stack
+      | DOPN(CoFix _,_) as c_0 -> c_0,stack
+      | DOPN(Fix (_) ,_) as fix -> 
+          let (reduced,(fix,stack')) = reduce_fix hnfstack fix stack in 
+	  if reduced then hnfstack fix stack' else raise Redelimination
+      | _ -> raise Redelimination
+  in 
+  hnfstack c stack
+
+(* Hnf reduction tactic: *)
+
+let hnf_constr env sigma c = 
+  let rec redrec x largs =
+    match x with
+      | DOP2(Lambda,t,DLAM(n,c)) ->
+          (match largs with
+             | []      -> applist(x,largs)
+             | a::rest -> stacklam redrec [a] c rest)
+      | DOPN(AppL,cl)   -> redrec (array_hd cl) (array_app_tl cl largs)
+      | DOPN(Const _,_) ->
+          (try
+             let (c',lrest) = red_elim_const env sigma x largs in 
+	     redrec c' lrest
+           with Redelimination ->
+             if evaluable_constant env x then
+               let c = constant_value env x in
+	       (match c with 
+                  | DOPN(CoFix _,_) -> applist(x,largs)
+		  | _ ->  redrec c largs)
+             else 
+	       applist(x,largs))
+      | DOPN(Abst _,_) ->
+          if evaluable_abst env x then 
+	    redrec (abst_value env x) largs
+          else 
+	    applist(x,largs)
+      | DOP2(Cast,c,_) -> redrec c largs
+      | DOPN(MutCase _,_) ->
+          let (ci,p,c,lf) = destCase x in
+          (try
+             redrec 
+	       (special_red_case env (whd_betadeltaiota_stack env sigma) 
+		  p c ci lf) largs
+           with Redelimination -> 
+	     applist(x,largs))
+      | (DOPN(Fix _,_)) ->
+          let (reduced,(fix,stack)) = 
+            reduce_fix (whd_betadeltaiota_stack env sigma) x largs
+          in 
+	  if reduced then redrec fix stack else applist(x,largs)
+      | _ -> applist(x,largs)
+  in 
+  redrec c []
+
+(* Simpl reduction tactic: same as simplify, but also reduces
+   elimination constants *)
+
+let whd_nf env sigma c = 
+  let rec nf_app c stack =
+    match c with
+      | DOP2(Lambda,c1,DLAM(name,c2))    ->
+          (match stack with
+             | [] -> (c,[])
+             | a1::rest -> stacklam nf_app [a1] c2 rest)
+      | DOPN(AppL,cl) -> nf_app (array_hd cl) (array_app_tl cl stack)
+      | DOP2(Cast,c,_) -> nf_app c stack
+      | DOPN(Const _,_) ->
+          (try
+             let (c',lrest) = red_elim_const env sigma c stack in 
+	     nf_app c' lrest
+           with Redelimination -> 
+	     (c,stack))
+      | DOPN(MutCase _,_) ->
+          let (ci,p,d,lf) = destCase c in
+          (try
+             nf_app (special_red_case env nf_app p d ci lf) stack
+           with Redelimination -> 
+	     (c,stack))
+      | DOPN(Fix _,_) ->
+          let (reduced,(fix,rest)) = reduce_fix nf_app c stack in 
+	  if reduced then nf_app fix rest else (fix,stack)
+      | _ -> (c,stack)
+  in 
+  applist (nf_app c [])
+
+let nf env sigma c = strong whd_nf env sigma c
+
+(* Generic reduction: reduction functions used in reduction tactics *)
+
+type red_expr =
+  | Red
+  | Hnf
+  | Simpl
+  | Cbv of Closure.flags
+  | Lazy of Closure.flags
+  | Unfold of (int list * section_path) list
+  | Fold of constr list
+  | Change of constr
+  | Pattern of (int list * constr * constr) list
+
+let reduction_of_redexp = function
+  | Red -> red_product
+  | Hnf -> hnf_constr
+  | Simpl -> nf
+  | Cbv f -> cbv_norm_flags f
+  | Lazy f -> clos_norm_flags f
+  | Unfold ubinds -> unfoldn ubinds
+  | Fold cl -> fold_commands cl
+  | Change t -> (fun _ _ _ -> t)
+  | Pattern lp -> pattern_occs lp
+
+(* Used in several tactics. *)
+
+let one_step_reduce env sigma = 
+  let rec redrec largs x =
+    match x with
+      | DOP2(Lambda,t,DLAM(n,c))  ->
+          (match largs with
+             | []      -> error "Not reducible 1"
+             | a::rest -> applistc (subst1 a c) rest)
+      | DOPN(AppL,cl) -> redrec (array_app_tl cl largs) (array_hd cl)
+      | DOPN(Const _,_) ->
+          (try
+             let (c',l) = red_elim_const env sigma x largs in applistc c' l
+           with Redelimination ->
+             if evaluable_constant env x then
+               applistc (constant_value env x) largs
+             else error "Not reductible 1")
+      | DOPN(Abst _,_) ->
+          if evaluable_abst env x then applistc (abst_value env x) largs
+          else error "Not reducible 0"
+      | DOPN(MutCase _,_) ->
+          let (ci,p,c,lf) = destCase x in
+          (try
+	     applistc 
+	       (special_red_case env (whd_betadeltaiota_stack env sigma) 
+		  p c ci lf) largs 
+           with Redelimination -> error "Not reducible 2")
+      | DOPN(Fix _,_) ->
+          let (reduced,(fix,stack)) = 
+	    reduce_fix (whd_betadeltaiota_stack env sigma) x largs
+          in 
+	  if reduced then applistc fix stack else error "Not reducible 3"
+      | DOP2(Cast,c,_) -> redrec largs c
+      | _ -> error "Not reducible 3"
+  in 
+  redrec []
+
+(* put t as t'=(x1:A1)..(xn:An)B with B an inductive definition of name name
+   return name, B and t' *)
+
+let reduce_to_mind env sigma t = 
+  let rec elimrec t l = 
+    match whd_castapp_stack t [] with
+      | (DOPN(MutInd _,_) as mind,_) -> (mind,t,prod_it t l)
+      | (DOPN(Const _,_),_) -> 
+          (try 
+	     let t' = nf_betaiota env sigma (one_step_reduce env sigma t) in 
+	     elimrec t' l
+           with UserError _ -> errorlabstrm "tactics__reduce_to_mind"
+               [< 'sTR"Not an inductive product : it is a constant." >])
+      | (DOPN(MutCase _,_),_) ->
+          (try 
+	     let t' = nf_betaiota env sigma (one_step_reduce env sigma t) in 
+	     elimrec t' l
+           with UserError _ -> errorlabstrm "tactics__reduce_to_mind"
+               [< 'sTR"Not an inductive product:"; 'sPC;
+		  'sTR"it is a case analysis term" >])
+      | (DOP2(Cast,c,_),[]) -> elimrec c l
+      | (DOP2(Prod,ty,DLAM(n,t')),[]) -> elimrec t' ((n,ty)::l)
+      | _ -> error "Not an inductive product"
+ in 
+ elimrec t []
+
+let reduce_to_ind env sigma t =
+  let (mind,redt,c) = reduce_to_mind env sigma t in 
+  (Declare.mind_path mind, redt, c)
+
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
new file mode 100644
index 0000000000..a1aec82cdd
--- /dev/null
+++ b/pretyping/tacred.mli
@@ -0,0 +1,38 @@
+
+(* $Id$ *)
+
+(*i*)
+open Names
+open Term
+open Environ
+open Evd
+open Reduction
+(*i*)
+
+(* Reduction functions associated to tactics. \label{tacred} *)
+
+val hnf_constr : 'a reduction_function
+
+val nf : 'a reduction_function
+
+val one_step_reduce : 'a reduction_function
+
+val reduce_to_mind : 
+  env -> 'a evar_map -> constr -> constr * constr * constr
+
+val reduce_to_ind : 
+  env -> 'a evar_map -> constr -> section_path * constr * constr
+
+type red_expr =
+  | Red
+  | Hnf
+  | Simpl
+  | Cbv of Closure.flags
+  | Lazy of Closure.flags
+  | Unfold of (int list * section_path) list
+  | Fold of constr list
+  | Change of constr
+  | Pattern of (int list * constr * constr) list
+
+val reduction_of_redexp : red_expr -> 'a reduction_function
+