index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
plugins
/
ltac
/
tacinterp.ml
Age
Commit message (
Expand
)
Author
2017-09-04
Making detyping potentially lazy.
Pierre-Marie Pédrot
2017-08-31
Merge PR #980: Adding combinators + a canonical renaming in List, Option, Name
Maxime Dénès
2017-08-29
Adapting code to renaming Option.fold_map -> Option.fold_left_map.
Hugo Herbelin
2017-08-29
Adapting code to renaming fold_map/fold_map' into fold_left_map/fold_right_map
Hugo Herbelin
2017-08-01
Move type_uconstr to Tacinterp.
Maxime Dénès
2017-07-26
Removing default evar-normalization for ARGUMENT EXTEND.
Pierre-Marie Pédrot
2017-07-25
[api] Remove type equalities from API.
Emilio Jesus Gallego Arias
2017-07-17
[API] Remove `open API` in ml files in favor of `-open API` flag.
Emilio Jesus Gallego Arias
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2017-06-14
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-11
[proof] Deprecate redundant wrappers.
Emilio Jesus Gallego Arias
2017-06-10
Remove (useless) aliases from the API.
Matej Košík
2017-06-09
A fix to #5414 (ident bound by ltac names now known for "match").
Hugo Herbelin
2017-06-07
Put all plugins behind an "API".
Matej Kosik
2017-06-06
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-05
Merge PR#590: A more explicit algebraic type for evars of kind MatchingVar + ...
Maxime Dénès
2017-06-02
Drop '.' from CErrors.anomaly, insert it in args
Jason Gross
2017-06-01
Merge PR#561: Improving the Name API
Maxime Dénès
2017-05-31
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-30
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-25
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-24
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-22
Clarifying the interpretation path for the "constr_with_binding" argument.
Hugo Herbelin
2017-05-03
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-04-27
Remove unused [open] statements
Gaetan Gilbert
2017-04-27
Remove some unused values and types
Gaetan Gilbert
2017-04-25
[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-24
[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-07
Merge branch 'master' into econstr
Pierre-Marie Pédrot
2017-03-24
Merge branch 'trunk' into pr379
Maxime Dénès
2017-03-23
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-17
Merge PR#428: Report missing tactic arguments in error message
Maxime Dénès
[next]
