diff options
| author | herbelin | 2003-09-23 11:18:22 +0000 |
|---|---|---|
| committer | herbelin | 2003-09-23 11:18:22 +0000 |
| commit | 090b29f754f44882a49961764e63be18f0d356c4 (patch) | |
| tree | c2cd77cc040a0730944ea586a0c591c7f676275f | |
| parent | 171a0af74fde8f05ac440491feb6acb76352b9e2 (diff) | |
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
| -rw-r--r-- | contrib/field/Field_Tactic.v | 8 |
1 files changed, 8 insertions, 0 deletions
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 ****) |