aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Collapse)AuthorAge
* [coqlib] Deprecate redundant Coqlib functions.Gravatar Emilio Jesus Gallego Arias2017-05-27
| | | | | | | | | | | | We remove redundant functions `coq_constant`, `gen_reference`, and `gen_constant`. This is a first step towards a lazy binding of libraries references. We have also chosen to untangle `constr` from `Coqlib`, as how to instantiate the reference (in particular wrt universes) is a client-side issue. (The client may want to provide an `evar_map` ?) c.f. #186
* Merge PR#666: romega revisited : no more normalization trace, cleaned-up ↵Gravatar Maxime Dénès2017-05-26
|\ | | | | | | resolution trace
* \ Merge PR#637: Short cleaning of the interpretation path for constr_with_bindingsGravatar Maxime Dénès2017-05-25
|\ \
* \ \ Merge PR#608: Allow Ltac2 as a pluginGravatar Maxime Dénès2017-05-25
|\ \ \
* \ \ \ Merge PR#481: [option] Remove support for non-synchronous options.Gravatar Maxime Dénès2017-05-25
|\ \ \ \
* \ \ \ \ Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\ \ \ \ \
| | | | | * ROmega: division-aware ReflOmegaCore, allowing trace without termsGravatar Pierre Letouzey2017-05-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The trace only mentions the constant k by which we want to divide the equation, not anymore the equation we obtain after the division. Shorter trace, and it won't take much more time to perform the few Z.div than checking as currently the equality of the initial equation and the final equation multiplied by k.
| | * | | | [option] Remove support for non-synchronous options.Gravatar Emilio Jesus Gallego Arias2017-05-24
| |/ / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Inspired by https://coq.inria.fr/bugs/show_bug.cgi?id=5229 , which this PR solves, I propose to remove support for non-synchronous options. It seems the few uses of `optsync = false` we legacy and shouldn't have any impact. Moreover, non synchronous options may create particularly tricky situations as for instance, they won't be propagated to workers.
| | | | * refl_omega: some code refactoringGravatar Pierre Letouzey2017-05-22
| | | | |
| | | | * refl_omega.v: explicitely identify atom indexes and omega varsGravatar Pierre Letouzey2017-05-22
| | | | |
| | | | * ReflOmegaCore: misc cleanup, <? instead of bgt, etcGravatar Pierre Letouzey2017-05-22
| | | | |
| | | | * ROmega : O_STATE turned into a O_SUMGravatar Pierre Letouzey2017-05-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We benefit from the fact that we normalize now *all* hypotheses even the one defining the "stated" variable: it is produced as ...def of v... = v and normalized as -v + ...def of v... = 0 which is precisely what we should add to the initial equation during a O_STATE.
| | | | * ROmega: less contructors in the final omega traceGravatar Pierre Letouzey2017-05-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Now that O_SUM is properly optimized (cf. the [fusion] function), we could use it to encode CONTRADICTION and NEGATE_CONTRADICT(_INV). This way, the trace has almost the same size, but ReflOmegaCore.v is shorter and easier to maintain.
| | | | * ROmega : merge O_CONSTANT* into a single O_BAD_CONSTANTGravatar Pierre Letouzey2017-05-22
| | | | |
| | | | * ReflOmegaCore: reverse some integer mult (coefs k1,k2 will often be simple)Gravatar Pierre Letouzey2017-05-22
| | | | |
| | | | * ReflOmegaCore: comment, reorganize, permut some constructors, etcGravatar Pierre Letouzey2017-05-22
| | | | |
| | | | * romega: add a tactic named unsafe_romega (for debugging, or bold users)Gravatar Pierre Letouzey2017-05-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In this variant, the proof term produced by romega isn't verified at the tactic run-time (no vm_compute). In theory, [unsafe_romega] should behave exactly as [romega], but faster. Now, if there's a bug in romega, we'll be notified only at the following Qed. This could be interesting for debugging purpose : you could inspect the produced buggish term via a Show Proof.
| | | | * romega: no more normalization trace, replaced by some Coq-side computationGravatar Pierre Letouzey2017-05-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a major change : - Generated proofs are quite shorter, since only the resolution trace remains. - No time penalty mesured (it even tends to be slightly faster this way). - Less infrastructure in ReflOmegaCore and refl_omega. - Warning: the normalization functions in ML and in Coq should be kept in sync, as well as the variable order. - Btw: get rid of ML constructor Oufo
| | | | * romega/const_omega : a few improvements (less try with, no gen equality)Gravatar Pierre Letouzey2017-05-22
| | | | |
| | | | * romega: use N instead of nat for TvarGravatar Pierre Letouzey2017-05-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In a coming commit, we'll normalize terms by a Coq function that will compare Tvar's instead of blindly applying a trace, so let's speed-up these comparisons.
| | | | * romega: shorter trace (no more term lengths)Gravatar Pierre Letouzey2017-05-22
| | | | |
| | | | * refl_omega: refactoring of normalize_equationGravatar Pierre Letouzey2017-05-22
| | | | |
| | | | * ReflOmegaCore: lots of dead code + a few refactored proofsGravatar Pierre Letouzey2017-05-22
| | | | |
| | | | * romega: if it bugs again, at least do it with a short and quick errorGravatar Pierre Letouzey2017-05-22
| | | | |
| | | | * refl_omega: comment the lack of lifts when dealing with arrowsGravatar Pierre Letouzey2017-05-22
| | | | |
| | | | * romega: discard constructor D_mono (shorter trace + fix a bug)Gravatar Pierre Letouzey2017-05-22
| | | | | | | | | | | | | | | | | | | | For the bug, see new test test_romega10 in test-suite/success/ROmega0.v.
| | | | * refl_omega: more refactoring (e.g. IntSets instead of sorted lists)Gravatar Pierre Letouzey2017-05-22
| | | | |
| | | | * refl_omega: refactoring (e.g. useless args in destructurate_pos_hyp)Gravatar Pierre Letouzey2017-05-22
| | | | |
| | | | * ReflOmegaCore: discard useless cosntructor P_NOPGravatar Pierre Letouzey2017-05-22
| | | | |
| | | | * ReflOmegaCore: revised proofs (mostly bullets instead of ;[|||])Gravatar Pierre Letouzey2017-05-22
| | |_|/ | |/| |
| | | * Using type classes in the interpretation of "specialize" and "contradiction".Gravatar Hugo Herbelin2017-05-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We do that by using constr_with_bindings rather than open_constr_with_bindings (+ extra call to typeclasses in "specialize"). If my understanding is right, the only effect would be to succeed more in cases where it was failing (in inh_conv_coerce_to_gen). In particular, "specialize" and "contradiction" already have a WITHHOLES test for rejecting pending holes. Incidentally, this answers enhancement #5153.
| | | * Clarifying the interpretation path for the "constr_with_binding" argument.Gravatar Hugo Herbelin2017-05-22
| | |/ | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This fixes an inconsistency introduced in 554a6c806 (svn r12603) where both interp_constr_with_bindings and interp_open_constr_with_bindings were going through interp_open_constr (no type classes so as to not to commit too early on irreversible choices, accepting unresolved holes). We fix this by having interp_constr_with_bindings going to interp_constr (using type classes and failing on unresolved evars). The external impact is that any TACTIC EXTEND which refers to constr_with_binding has now to decide whether it intends it to use what the name suggest (using type classes and to fail if evars remain unresolved), thus keeping constr_with_binding, or the actual behavior which requires to use open_constr_with_bindings for strict compatibility.
| | * Merge branch 'master' into ltac2-hooksGravatar Pierre-Marie Pédrot2017-05-19
| | |\
| * | | Add .dir-locals.el to pluginsGravatar Jason Gross2017-05-18
| | |/ | |/| | | | | | | | | | As requested in https://github.com/coq/coq/pull/386#issuecomment-302358542
| * | Merge PR#633: An extension of EXTEND and notations to make standard parsing ↵Gravatar Maxime Dénès2017-05-17
| |\ \ | | | | | | | | | | | | tricks available to users
| * \ \ Merge PR#607: Make congruence reuse discriminate instead of rolling its own.Gravatar Maxime Dénès2017-05-17
| |\ \ \
| | | * | Fixing grammar for "evar" by exporting the test_lpar_id_colon trick to EXTEND.Gravatar Hugo Herbelin2017-05-16
| | | | |
| | | * | Adding support for using grammar entries returning no value in EXTEND.Gravatar Hugo Herbelin2017-05-16
| | | | |
| * | | | Typo in a comment of plugin Quote.Gravatar Hugo Herbelin2017-05-13
| | |/ / | |/| |
| * | | Merge PR#201: Transparent abstractGravatar Maxime Dénès2017-05-11
| |\ \ \
| * \ \ \ Merge PR#612: Set Ltac Batch DebugGravatar Maxime Dénès2017-05-09
| |\ \ \ \
| * | | | | Prevent user-defined ring morphisms from ever being evaluated.Gravatar Guillaume Melquiond2017-05-09
| | | | | |
| | * | | | Adding an option "Set Ltac Batch Debug" to additionally run Ltac debug in ↵Gravatar Hugo Herbelin2017-05-04
| |/ / / / | | | | | | | | | | | | | | | batch mode.
| | | | * Generalizing the tactic-in-term embedding to any generic argument.Gravatar Pierre-Marie Pédrot2017-05-03
| | | | |
| | | | * Allowing to pass arbitrary data in internalization environments.Gravatar Pierre-Marie Pédrot2017-05-03
| | |_|/ | |/| |
| | | * Make congruence reuse discriminate instead of rolling its own.Gravatar Gaetan Gilbert2017-05-03
| | |/ | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This changes the produced terms a bit, eg Axiom T : Type. Lemma foo : true = false -> T. Proof. congruence. Qed. used to produce fun H : true = false => let Heq := H : true = false in @eq_rect Type True (fun X : Type => X) I T (@f_equal bool Type (fun t : bool => if t then True else T) true false Heq) now produces fun H : true = false => let Heq : true = false := H in let H0 : False := @eq_ind bool true (fun e : bool => if e then True else False) I false Heq in False_rect T H0 i.e. instead of proving [True = T] by [f_equal] then transporting [I] across this identity, it now proves [False] by [eq_ind] then uses exfalso.
| * | Post-rebase warnings (unused opens and 2 unused values)Gravatar Gaetan Gilbert2017-04-27
| | |
| * | Fix 4.04 warningsGravatar Gaetan Gilbert2017-04-27
| | |
| * | Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
| | |
| * | Micromega: do not use Filename.temp_dir_path, remove unused valuesGravatar Gaetan Gilbert2017-04-27
| | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 05:13:13 +0000