diff options
| -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 ****) |