From 3c8212912600744b79b328b9105219acbb38ae17 Mon Sep 17 00:00:00 2001
From: coq
Date: Fri, 16 Sep 2005 20:49:38 +0000
Subject: changed the syntax categories of arguments of functional scheme
 (constr --> ident). Transparent for the user.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7383 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/funind/tacinv.ml4 | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/contrib/funind/tacinv.ml4 b/contrib/funind/tacinv.ml4
index 3e82dcbd1e..d06d396640 100644
--- a/contrib/funind/tacinv.ml4
+++ b/contrib/funind/tacinv.ml4
@@ -825,9 +825,10 @@ let buildFunscheme fonc mutflist =
     
 (* Declaration of the functional scheme. *)
 let declareFunScheme f fname mutflist =
+ let id_to_cstr = constr_of_id (Global.env()) in (* careful: env() is evaluated now *)
  let flist = if mutflist=[] then [f] else mutflist in
- let fcstrlist = Array.of_list (List.map constr_of flist) in
- let scheme = buildFunscheme (constr_of f) fcstrlist in
+ let fcstrlist = Array.of_list (List.map id_to_cstr flist) in
+ let scheme = buildFunscheme (id_to_cstr f) fcstrlist in
   let _ = prstr "Principe:" in
   let _ = prconstr scheme in
  let ce = { 
@@ -842,9 +843,9 @@ let declareFunScheme f fname mutflist =
 
 VERNAC COMMAND EXTEND FunctionalScheme
  [ "Functional" "Scheme" ident(na) ":=" "Induction" "for" 
-    constr(c) "with" ne_constr_list(l) ]
+    ident(c) "with" ne_ident_list(l) ] 
   -> [ declareFunScheme c na l ]
-| [ "Functional" "Scheme" ident(na) ":=" "Induction" "for" constr(c) ]
+| [ "Functional" "Scheme" ident(na) ":=" "Induction" "for" ident (c) ]
   -> [ declareFunScheme c na [] ]
 END
 
-- 
cgit v1.2.3