diff options
| author | filliatr | 1999-11-19 17:01:43 +0000 |
|---|---|---|
| committer | filliatr | 1999-11-19 17:01:43 +0000 |
| commit | 9bdaa212057cdd41ba416cc9f05167e91eeed4b3 (patch) | |
| tree | 328de03d16931d5abfd9ac4c0254b93cb0e5dcf9 /proofs | |
| parent | b0382a9829f08282351244839526bd2ffbe6283f (diff) | |
module Pattern, Wcclausenv (interface) et Tacticals
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@126 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/logic.ml | 2 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 2 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 1 | ||||
| -rw-r--r-- | proofs/tacred.mli | 1 |
4 files changed, 5 insertions, 1 deletions
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 |