diff options
| author | Hugo Herbelin | 2020-03-22 12:30:55 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-04-03 20:33:27 +0200 |
| commit | aa889ee516453af65bd74ffedf8ec3761f97eb43 (patch) | |
| tree | 9dbe0527c1fc7dd34eb8fa9a2462d3a96048baaa /theories/micromega | |
| parent | 9e98c1ebb9472f1c77eb0289bd64e525d58d99de (diff) | |
Avoiding using a fixed introduction name in Ltac code of stdlib.
Diffstat (limited to 'theories/micromega')
| -rw-r--r-- | theories/micromega/Lia.v | 2 | ||||
| -rw-r--r-- | theories/micromega/Lqa.v | 2 | ||||
| -rw-r--r-- | theories/micromega/Lra.v | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/theories/micromega/Lia.v b/theories/micromega/Lia.v index f3b70f61d2..3d955fec4f 100644 --- a/theories/micromega/Lia.v +++ b/theories/micromega/Lia.v @@ -21,7 +21,7 @@ Declare ML Module "micromega_plugin". Ltac zchecker := - intros __wit __varmap __ff ; + intros ?__wit ?__varmap ?__ff ; exact (ZTautoChecker_sound __ff __wit (@eq_refl bool true <: @eq bool (ZTautoChecker __ff __wit) true) (@find Z Z0 __varmap)). diff --git a/theories/micromega/Lqa.v b/theories/micromega/Lqa.v index 786c9275f0..8a4d59b1bd 100644 --- a/theories/micromega/Lqa.v +++ b/theories/micromega/Lqa.v @@ -23,7 +23,7 @@ Require Coq.micromega.Tauto. Declare ML Module "micromega_plugin". Ltac rchange := - intros __wit __varmap __ff ; + intros ?__wit ?__varmap ?__ff ; change (Tauto.eval_bf (Qeval_formula (@find Q 0%Q __varmap)) __ff) ; apply (QTautoChecker_sound __ff __wit). diff --git a/theories/micromega/Lra.v b/theories/micromega/Lra.v index 3ac4772ba4..22cef50e0d 100644 --- a/theories/micromega/Lra.v +++ b/theories/micromega/Lra.v @@ -23,7 +23,7 @@ Require Coq.micromega.Tauto. Declare ML Module "micromega_plugin". Ltac rchange := - intros __wit __varmap __ff ; + intros ?__wit ?__varmap ?__ff ; change (Tauto.eval_bf (Reval_formula (@find R 0%R __varmap)) __ff) ; apply (RTautoChecker_sound __ff __wit). |