From 426767b93914a2d2347eff6c7dbc6d22e5be36ef Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 9 Nov 2003 12:52:25 +0000
Subject: Ajout reduce_to_quantified_ref

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4835 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/tacred.ml  | 18 ++++++++++++++++++
 pretyping/tacred.mli |  5 +++++
 2 files changed, 23 insertions(+)

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
-- 
cgit v1.2.3