index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
tactics
/
tacinterp.ml
Age
Commit message (
Expand
)
Author
2009-12-23
Moved a bit further the code for pattern interpretation in match goal
herbelin
2009-12-21
Generic support for open terms in tactics
herbelin
2009-10-28
Make usage of Dyn explicit
glondu
2009-10-26
New cleaning phase of the Local/Global option management
herbelin
2009-10-21
This big commit addresses two problems:
soubiran
2009-10-06
Relaxed error severity when encountering unknown library objects or tactic
gmelquio
2009-09-27
Apply "Declare Implicit Tactic" also to terms interpreted as "open
herbelin
2009-09-26
Fixed a hole in glob_tactic that allowed some Ltac code to refer to
herbelin
2009-09-20
Only one "in" clause in "destruct" even for a multiple "destruct".
herbelin
2009-09-17
Remove useless Liboject.export_function field
glondu
2009-09-17
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-11
Generalized the possibility to refer to a global name by a notation
herbelin
2009-09-10
Added syntax "exists bindings, ..., bindings" for iterated "exists".
herbelin
2009-08-13
Death of "survive_module" and "survive_section" (the first one was
herbelin
2009-08-06
- Cleaning phase of the interfaces of libnames.ml and nametab.ml
herbelin
2009-08-04
- Add more precise error localisation when one of the application fails
herbelin
2009-08-03
Added "etransitivity".
herbelin
2009-07-07
Jolification : tentative de supprimer les "( evd)" et associés qui
aspiwack
2009-06-30
Add new variants of [rewrite] and [autorewrite] which differ in the
msozeau
2009-06-11
Use a lazy value for the message in FailError, so that it won't be
msozeau
2009-06-07
- Added two new introduction patterns with the following temptative syntaxes:
herbelin
2009-05-10
- Addition of "Hint Resolve ->" and "Hint Resolve <-" continued: it
herbelin
2009-05-09
- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence
herbelin
2009-04-27
- Fixed a little bug in previous commit (bad failure in case of unknown entry).
herbelin
2009-04-27
- Cleaning (unification of ML names, removal of obsolete code,
herbelin
2009-04-24
Fixing bug #2308 ("instantiate" tactic did not comply with
herbelin
2009-04-16
nouvelle version de la tactique groebner proposee par Loic:
barras
2009-04-05
Display the content of the list instead of "<list>" when an idtac
herbelin
2009-03-28
Fix useless redeclaration of a tactic name when UpdateTac is replayed.
msozeau
2009-03-22
Backport from v8.2 branch of 11986 (interpretation of quantified
herbelin
2009-03-19
coq_makefile: -c and -shared conflict; tacinterp: delay evaluation of tactic ...
barras
2009-03-17
- gros commit sur ring et field: passage des arguments simplifie
barras
2009-03-04
illegal tactic application was having Ltac interpreter loop
barras
2009-03-04
commande Timeout + compaction des traces de debug_tactic
barras
2009-03-04
Backtrack sur la mémoïsation de nf_evar.
aspiwack
2009-02-27
=?utf-8?q?Tentative=20d'optimisation=20(en=20temps)=20sur=20[nf=5Fevar]=20et=...
aspiwack
2009-02-19
On remplace evar_map par evar_defs (seul evar_defs est désormais exporté
aspiwack
2009-01-04
Fixed bugs #2001 (search_guard was overwriting the guard index given
herbelin
2009-01-02
- Temptative change to notations like "as [|n H]_eqn" or "as [|n H]_eqn:H",
herbelin
2008-12-29
- Added support for subterm matching in SearchAbout.
herbelin
2008-12-09
About "apply in":
herbelin
2008-11-05
Port [rewrite] tactics to open terms. Currently no check that evars
msozeau
2008-10-25
More debugging of handling of open constrs with typeclasses:
msozeau
2008-10-23
Forgot one file which had other local modifications...
msozeau
2008-10-19
- Export de pattern_ident vers les ARGUMENT EXTEND and co.
herbelin
2008-10-18
Optimisation de clenv.ml pour que meta_instance ne soit pas appelé
herbelin
2008-10-11
Backporting 11445 from 8.2 to trunk (negative conditions in
herbelin
2008-08-05
Correction de bugs:
herbelin
2008-08-04
Évolutions diverses et variées.
herbelin
2008-07-24
Propagation de l'information "strict" (càd à toplevel ou en train de
herbelin
[prev]
[next]