From 090b29f754f44882a49961764e63be18f0d356c4 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 23 Sep 2003 11:18:22 +0000
Subject: Ajout fonctions syntaxe v8 pour contrib MapleMode

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4457 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/field/Field_Tactic.v | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/contrib/field/Field_Tactic.v b/contrib/field/Field_Tactic.v
index beb6d10efa..cd382bc393 100644
--- a/contrib/field/Field_Tactic.v
+++ b/contrib/field/Field_Tactic.v
@@ -63,6 +63,10 @@ Tactic Definition Number lvar := (NumberAux lvar O).
 Tactic Definition BuildVarList FT trm :=
   Let lvar = (SeekVar FT trm) In
   (Number lvar).
+V7only [
+(*Used by contrib Maple *)
+Tactic Definition build_var_list := BuildVarList.
+].
 
 Recursive Tactic Definition Assoc elt lst :=
   Match lst With
@@ -282,6 +286,10 @@ Meta Definition InitExp FT trm :=
   Match Eval Cbv Beta Delta [Adiv] Iota in (Adiv FT) With
   | [(Some ? ?1)] -> Eval Cbv Beta Delta [?1] in e
   | _ -> e.
+V7only [
+(*Used by contrib Maple *)
+Tactic Definition init_exp := InitExp.
+].
 
 (**** Inverses simplification ****)
 
-- 
cgit v1.2.3