From 15da5979d322c5da5f251dfd92da26407df5e45f Mon Sep 17 00:00:00 2001
From: barras
Date: Wed, 9 Oct 2002 15:42:49 +0000
Subject: retour en arriere concernant la recherche d'occurence modulo
 expansion des letins, ce qui conduisait a des comportement peu intuitifs. On
 priviligiera l'utilisation de la tactique Subst.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3110 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/termops.mli | 17 ++++++-----------
 1 file changed, 6 insertions(+), 11 deletions(-)

(limited to 'pretyping/termops.mli')

diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 431e69e7f0..95d769c43f 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -73,10 +73,6 @@ val free_rels : constr -> Intset.t
 (* Substitution of metavariables *)
 val subst_meta : (int * constr) list -> constr -> constr
 
-(* Expansion of local definitions *)
-val whd_locals : env -> constr -> constr
-val nf_locals  : env -> constr -> constr
-
 (* [pop c] lifts by -1 the positive indexes in [c] *)
 val pop : constr -> constr
 
@@ -84,20 +80,19 @@ val pop : constr -> constr
    reduction of let *)
 val dependent : constr -> constr -> bool
 val subst_term_gen :
-  (env -> constr -> constr -> bool) -> env -> constr -> constr -> constr
+  (constr -> constr -> bool) -> constr -> constr -> constr
 val replace_term_gen :
-  (env -> constr -> constr -> bool) ->
-    env -> constr -> constr -> constr -> constr
+  (constr -> constr -> bool) ->
+    constr -> constr -> constr -> constr
 val subst_term : constr -> constr -> constr
 val replace_term : constr -> constr -> constr -> constr
 val subst_term_occ_gen :
-  env -> int list -> int -> constr -> types -> int * types
-val subst_term_occ : env -> int list -> constr -> types -> types
+  int list -> int -> constr -> types -> int * types
+val subst_term_occ : int list -> constr -> types -> types
 val subst_term_occ_decl :
-  env -> int list -> constr -> named_declaration -> named_declaration
+  int list -> constr -> named_declaration -> named_declaration
 
 (* Alternative term equalities *)
-val zeta_eq_constr : constr -> constr -> bool
 val eta_reduce_head : constr -> constr
 val eta_eq_constr : constr -> constr -> bool
 
-- 
cgit v1.2.3