diff options
| author | herbelin | 2001-09-09 20:52:02 +0000 |
|---|---|---|
| committer | herbelin | 2001-09-09 20:52:02 +0000 |
| commit | 69c20900c67c53c9c3b4e000181b903f86929d1b (patch) | |
| tree | e8a443ba49c7d87358a3f2f8f9d817d06fb58f53 /proofs | |
| parent | 14e2cba128e83e7d1289b5d4bb3c702ff3d219b6 (diff) | |
Nettoyage reduce_to_ind et one_step_reduce
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1942 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/tacmach.ml | 5 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 8 |
2 files changed, 5 insertions, 8 deletions
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 69697c809f..d2f12d3523 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -108,9 +108,8 @@ let pf_type_of = pf_reduce type_of let pf_conv_x = pf_reduce is_conv let pf_conv_x_leq = pf_reduce is_conv_leq let pf_const_value = pf_reduce (fun env _ -> constant_value env) -let pf_one_step_reduce = pf_reduce one_step_reduce -let pf_reduce_to_mind = pf_reduce reduce_to_mind -let pf_reduce_to_ind = pf_reduce reduce_to_ind +let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind +let pf_reduce_to_atomic_ind = pf_reduce reduce_to_atomic_ind let hnf_type_of gls = compose (pf_whd_betadeltaiota gls) (pf_type_of gls) diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 721f847243..930588fcb8 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -73,11 +73,9 @@ 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 -> inductive * constr * constr -val pf_reduce_to_ind : - goal sigma -> constr -> section_path * constr * constr -val pf_compute : goal sigma -> constr -> constr +val pf_reduce_to_quantified_ind : goal sigma -> types -> inductive * types +val pf_reduce_to_atomic_ind : goal sigma -> types -> inductive * types +val pf_compute : goal sigma -> constr -> constr val pf_unfoldn : (int list * Closure.evaluable_global_reference) list -> goal sigma -> constr -> constr |