From 9bdaa212057cdd41ba416cc9f05167e91eeed4b3 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Fri, 19 Nov 1999 17:01:43 +0000
Subject: module Pattern, Wcclausenv (interface) et Tacticals

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@126 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/logic.ml    | 2 +-
 proofs/tacmach.ml  | 2 ++
 proofs/tacmach.mli | 1 +
 proofs/tacred.mli  | 1 +
 4 files changed, 5 insertions(+), 1 deletion(-)

(limited to 'proofs')

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 21bfb2d71e..7056dadf17 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -409,7 +409,7 @@ let extract_constr =
               | GLOBNAME (id,_) -> VAR id
               | RELNAME (n,_) -> Rel n)
          with Not_found -> 
-           (try global_reference str
+           (try global_reference CCI str
             with Not_found -> error ((string_of_id str)^" not declared")))
 	
     | (Rel _) as val_0 -> val_0
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index a889e668c9..f3054b3cc7 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -73,11 +73,13 @@ let pf_reduction_of_redexp gls re c =
   reduction_of_redexp re (pf_env gls) (project gls) c 
 
 let pf_reduce redfun gls c       = redfun (pf_env gls) (project gls) c 
+
 let pf_whd_betadeltaiota         = pf_reduce whd_betadeltaiota
 let pf_whd_betadeltaiota_stack   = pf_reduce whd_betadeltaiota_stack
 let pf_hnf_constr                = pf_reduce hnf_constr
 let pf_red_product               = pf_reduce red_product
 let pf_nf                        = pf_reduce nf
+let pf_nf_betaiota               = pf_reduce nf_betaiota
 let pf_compute                   = pf_reduce compute
 let pf_unfoldn ubinds            = pf_reduce (unfoldn ubinds)
 
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 07a7be00c7..a3480cc18d 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -53,6 +53,7 @@ val pf_whd_betadeltaiota_stack : goal sigma -> 'a stack_reduction_function
 val pf_hnf_constr              : goal sigma -> constr -> constr
 val pf_red_product             : goal sigma -> constr -> constr
 val pf_nf                      : goal sigma -> constr -> constr
+val pf_nf_betaiota             : goal sigma -> constr -> constr
 val pf_one_step_reduce         : goal sigma -> constr -> constr
 val pf_reduce_to_mind : goal sigma -> constr -> constr * constr * constr
 val pf_reduce_to_ind  : goal sigma  -> constr -> section_path * constr * constr
diff --git a/proofs/tacred.mli b/proofs/tacred.mli
index f932cf66ed..59069fc046 100644
--- a/proofs/tacred.mli
+++ b/proofs/tacred.mli
@@ -19,6 +19,7 @@ val one_step_reduce : 'a reduction_function
 
 val reduce_to_mind : 
   unsafe_env -> 'a evar_map -> constr -> constr * constr * constr
+
 val reduce_to_ind : 
   unsafe_env -> 'a evar_map -> constr -> section_path * constr * constr
 
-- 
cgit v1.2.3