From 07e03e167c7eda30ffc989530470b5c597beaedc Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 15 Apr 2008 12:00:50 +0000
Subject: - Un peu de doc, préparation du CHANGES pour la release. -
 Re-restriction de inversion (après la correction des bugs - et   notamment du
 "Unknown meta" qui apparaissait parfois -, inversion   devenait capable
 d'agir sur des buts non atomiques, ce qui crée   quelques incompatibilités,
 typiquement dans CoRN où inversion est   utilisé dans un rôle de
 discriminate; en attendant de voir, on   revient à la sémantique initiale). -
 Généralisation de Local/Global dans Implicit Arguments pour avoir un  
 fonctionnement plus uniforme et plus facile à documenter. - Code mort
 (clenv.ml).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10796 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/inv.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/inv.ml b/tactics/inv.ml
index 03eaf2d4d0..a77a979060 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -450,7 +450,7 @@ let raw_inversion inv_kind id status names gl =
   let env = pf_env gl and sigma = project gl in
   let c = mkVar id in
   let (ind,t) = 
-    try pf_reduce_to_quantified_ind gl (pf_type_of gl c)
+    try pf_reduce_to_atomic_ind gl (pf_type_of gl c)
     with UserError _ -> 
       errorlabstrm "raw_inversion"
 	(str ("The type of "^(string_of_id id)^" is not inductive")) in
-- 
cgit v1.2.3