Ajout reduce_to_quantified_ref

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

2 files changed, 23 insertions, 0 deletions

diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 1e25cc195b..09f552ba15 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -907,3 +907,21 @@ let reduce_to_ind_gen allow_product env sigma t =
 
 let reduce_to_quantified_ind x = reduce_to_ind_gen true x
 let reduce_to_atomic_ind x = reduce_to_ind_gen false x
+
+let reduce_to_quantified_ref env sigma ref t = 
+  let rec elimrec env t l = 
+    let c, _ = Reductionops.whd_stack t in
+    match kind_of_term c with
+      | Prod (n,ty,t') -> elimrec (push_rel (n,None,t) env) t' ((n,None,ty)::l)
+      | _ ->
+	  try 
+	    if reference_of_constr c = ref 
+	    then it_mkProd_or_LetIn t l
+	    else raise Not_found
+	  with Not_found ->
+          try 
+	    let t' = nf_betaiota (one_step_reduce env sigma t) in 
+	    elimrec env t' l
+          with NotStepReducible -> raise Not_found
+  in
+  elimrec env t []
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index 9d76b655c7..c97a27f6ad 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -61,6 +61,11 @@ val reduce_to_atomic_ind : env ->  evar_map -> types -> inductive * types
    returns [I] and [t'] or fails with a user error *)
 val reduce_to_quantified_ind : env ->  evar_map -> types -> inductive * types
 
+(* [reduce_to_quantified_ref env sigma ref t] try to put [t] in the form
+   [t'=(x1:A1)..(xn:An)(ref args)] and raise Not_found if not possible *)
+val reduce_to_quantified_ref :
+  env ->  evar_map -> Libnames.global_reference -> types -> types
+
 type red_expr = (constr, evaluable_global_reference) red_expr_gen
 
 val contextually : constr occurrences -> reduction_function->reduction_function