From d21d934c5ef9f47046a705eebd554e63f77b9e30 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Mon, 13 Dec 1999 15:23:16 +0000
Subject:  - états fabriqués avec -silent  - compilation theories avec -q  -
 correction but de tclORELSE qui doit maintenant rattraper aussi    TypeError
 et RefinerError

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@249 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/tacred.ml  | 2 --
 pretyping/tacred.mli | 1 -
 2 files changed, 3 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 16ea6c5896..ad33549ca6 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -270,7 +270,6 @@ type red_expr =
   | Lazy of Closure.flags
   | Unfold of (int list * section_path) list
   | Fold of constr list
-  | Change of constr
   | Pattern of (int list * constr * constr) list
 
 let reduction_of_redexp = function
@@ -281,7 +280,6 @@ let reduction_of_redexp = function
   | Lazy f -> clos_norm_flags f
   | Unfold ubinds -> unfoldn ubinds
   | Fold cl -> fold_commands cl
-  | Change t -> (fun _ _ _ -> t)
   | Pattern lp -> pattern_occs lp
 
 (* Used in several tactics. *)
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index a1aec82cdd..a555667e6d 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -31,7 +31,6 @@ type red_expr =
   | Lazy of Closure.flags
   | Unfold of (int list * section_path) list
   | Fold of constr list
-  | Change of constr
   | Pattern of (int list * constr * constr) list
 
 val reduction_of_redexp : red_expr -> 'a reduction_function
-- 
cgit v1.2.3