index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
plugins
/
ltac
/
tacinterp.ml
Commit message (
Expand
)
Author
Age
*
Merge PR#763: [proof] Deprecate redundant wrappers.
Maxime Dénès
2017-06-14
|
\
*
\
Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match").
Maxime Dénès
2017-06-14
|
\
\
|
|
*
[proof] Deprecate redundant wrappers.
Emilio Jesus Gallego Arias
2017-06-11
*
|
|
Remove (useless) aliases from the API.
Matej Košík
2017-06-10
|
|
/
|
/
|
|
*
A fix to #5414 (ident bound by ltac names now known for "match").
Hugo Herbelin
2017-06-09
|
/
*
Put all plugins behind an "API".
Matej Kosik
2017-06-07
*
Remove the Sigma (monotonous state) API.
Maxime Dénès
2017-06-06
*
Merge PR#600: Some factorizations of ltac interpretation functions between ss...
Maxime Dénès
2017-06-06
|
\
*
\
Merge PR#716: Don't double up on periods in anomalies
Maxime Dénès
2017-06-06
|
\
\
*
\
\
Merge PR#590: A more explicit algebraic type for evars of kind MatchingVar + ...
Maxime Dénès
2017-06-05
|
\
\
\
|
|
*
|
Drop '.' from CErrors.anomaly, insert it in args
Jason Gross
2017-06-02
|
|
/
/
|
/
|
|
*
|
|
Merge PR#561: Improving the Name API
Maxime Dénès
2017-06-01
|
\
\
\
|
|
*
|
Renaming allow_patvar flag of intern_gen into pattern_mode.
Hugo Herbelin
2017-05-31
|
|
|
*
Factorizing interp_gen through a function interpreting glob_constr.
Hugo Herbelin
2017-05-31
|
|
|
*
Splitting interp_open_constr into two variants, with or without type classes.
Hugo Herbelin
2017-05-31
|
|
|
/
|
*
/
Creating a module Nameops.Name extending module Names.Name.
Hugo Herbelin
2017-05-31
|
|
/
*
|
Adding "epose", "eset", "eremember" which allow to set terms with
Hugo Herbelin
2017-05-30
*
|
Adding "eassert", "eenough", "epose proof", which allow to state
Hugo Herbelin
2017-05-30
|
/
*
Merge PR#637: Short cleaning of the interpretation path for constr_with_bindings
Maxime Dénès
2017-05-25
|
\
*
\
Merge PR#608: Allow Ltac2 as a plugin
Maxime Dénès
2017-05-25
|
\
\
*
\
\
Merge PR#481: [option] Remove support for non-synchronous options.
Maxime Dénès
2017-05-25
|
\
\
\
*
\
\
\
Merge branch 'trunk' into located_switch
Emilio Jesus Gallego Arias
2017-05-24
|
\
\
\
\
|
|
*
|
|
[option] Remove support for non-synchronous options.
Emilio Jesus Gallego Arias
2017-05-24
|
|
/
/
/
|
|
|
*
Clarifying the interpretation path for the "constr_with_binding" argument.
Hugo Herbelin
2017-05-22
|
|
|
/
|
|
/
|
|
|
*
Generalizing the tactic-in-term embedding to any generic argument.
Pierre-Marie Pédrot
2017-05-03
|
|
*
Allowing to pass arbitrary data in internalization environments.
Pierre-Marie Pédrot
2017-05-03
|
|
/
|
*
Remove unused [open] statements
Gaetan Gilbert
2017-04-27
|
*
Remove some unused values and types
Gaetan Gilbert
2017-04-27
*
|
[location] [ast] Port module AST to CAst
Emilio Jesus Gallego Arias
2017-04-25
*
|
[location] [ast] Switch Constrexpr AST to an extensible node type.
Emilio Jesus Gallego Arias
2017-04-25
*
|
[location] Make location optional in Loc.located
Emilio Jesus Gallego Arias
2017-04-25
*
|
[location] Remove Loc.ghost.
Emilio Jesus Gallego Arias
2017-04-25
*
|
[location] Use located in tactics.
Emilio Jesus Gallego Arias
2017-04-24
*
|
[location] Use located in misctypes.
Emilio Jesus Gallego Arias
2017-04-24
*
|
[location] Switch glob_constr to Loc.located
Emilio Jesus Gallego Arias
2017-04-24
*
|
[location] Use Loc.located for constr_expr.
Emilio Jesus Gallego Arias
2017-04-24
|
/
*
Merge branch 'master' into econstr
Pierre-Marie Pédrot
2017-04-07
|
\
*
|
Merge branch 'trunk' into pr379
Maxime Dénès
2017-03-24
|
*
Fast path for implicit tactic solving.
Pierre-Marie Pédrot
2017-03-23
|
*
Ensuring static invariants about handling of pending evars in Pretyping.
Pierre-Marie Pédrot
2017-03-23
|
/
*
Merge PR#428: Report missing tactic arguments in error message
Maxime Dénès
2017-03-17
|
\
*
|
Attempt to improve error message when "apply in" fail.
Hugo Herbelin
2017-03-15
|
*
Report missing tactic arguments in error message
Tej Chajed
2017-03-14
|
/
*
Merge PR#432: [cleanup] Change Id.t option to Name.t in TacFun
Maxime Dénès
2017-03-14
*
Merge PR#395: Allow hintdb to be parameters in a Ltac definition or
Maxime Dénès
2017-02-27
*
Ltac as a plugin.
Pierre-Marie Pédrot
2017-02-17