diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
commit | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (patch) | |
tree | 26dd9c4aa142597ee09c887ef161d5f0fa5077b6 /theories/Numbers/Natural/BigN/BigN.v | |
parent | 164c6861860e6b52818c031f901ffeff91fca16a (diff) |
Imported Upstream version 8.6upstream/8.6
Diffstat (limited to 'theories/Numbers/Natural/BigN/BigN.v')
-rw-r--r-- | theories/Numbers/Natural/BigN/BigN.v | 26 |
1 files changed, 13 insertions, 13 deletions
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v index 29a1145e..e8ff516f 100644 --- a/theories/Numbers/Natural/BigN/BigN.v +++ b/theories/Numbers/Natural/BigN/BigN.v @@ -110,7 +110,7 @@ intros NEQ. generalize (BigN.spec_div_eucl a b). generalize (Z_div_mod_full [a] [b] NEQ). destruct BigN.div_eucl as (q,r), Z.div_eucl as (q',r'). -intros (EQ,_). injection 1. intros EQr EQq. +intros (EQ,_). injection 1 as EQr EQq. BigN.zify. rewrite EQr, EQq; auto. Qed. @@ -119,10 +119,10 @@ Qed. Ltac isStaticWordCst t := match t with - | W0 => constr:true + | W0 => constr:(true) | WW ?t1 ?t2 => match isStaticWordCst t1 with - | false => constr:false + | false => constr:(false) | true => isStaticWordCst t2 end | _ => isInt31cst t @@ -139,30 +139,30 @@ Ltac isBigNcst t := | BigN.N6 ?t => isStaticWordCst t | BigN.Nn ?n ?t => match isnatcst n with | true => isStaticWordCst t - | false => constr:false + | false => constr:(false) end - | BigN.zero => constr:true - | BigN.one => constr:true - | BigN.two => constr:true - | _ => constr:false + | BigN.zero => constr:(true) + | BigN.one => constr:(true) + | BigN.two => constr:(true) + | _ => constr:(false) end. Ltac BigNcst t := match isBigNcst t with - | true => constr:t - | false => constr:NotConstant + | true => constr:(t) + | false => constr:(NotConstant) end. Ltac BigN_to_N t := match isBigNcst t with | true => eval vm_compute in (BigN.to_N t) - | false => constr:NotConstant + | false => constr:(NotConstant) end. Ltac Ncst t := match isNcst t with - | true => constr:t - | false => constr:NotConstant + | true => constr:(t) + | false => constr:(NotConstant) end. (** Registration for the "ring" tactic *) |