index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
proofs
/
proof_type.ml
Commit message (
Expand
)
Author
Age
*
Removing dead code.
Pierre-Marie Pédrot
2015-02-02
*
Update headers.
Maxime Dénès
2015-01-12
*
Removing useless flag of the historical move tactic.
Pierre-Marie Pédrot
2014-11-22
*
Removing the legacy intro tactic code.
Pierre-Marie Pédrot
2014-11-07
*
Removing the old rename tactic.
Pierre-Marie Pédrot
2014-11-04
*
Removing Convert_concl and Convert_hyp from Logic.
Hugo Herbelin
2014-10-09
*
Fixing localisation of tactic errors (my mistake in himsg.ml essentially).
Hugo Herbelin
2014-09-10
*
Removing the old implementation of clear_body.
Pierre-Marie Pédrot
2014-09-05
*
Revert the two previous commits. I was testing in the wrong branch.
Pierre-Marie Pédrot
2014-09-04
*
Removing the old implementation of clear_body.
Pierre-Marie Pédrot
2014-09-04
*
Removing dead code, thanks to new OCaml warnings and a bit of scripting.
Pierre-Marie Pédrot
2014-04-23
*
Removing the Change_evar refiner rule.
Pierre-Marie Pédrot
2014-03-31
*
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2014-03-05
*
Removing a fishy use of pervasive equality in Ltac backtrace printing.
Pierre-Marie Pédrot
2014-03-01
*
Do not print tactic notation names at each interpretation step.
ppedrot
2013-11-12
*
Generalizing the use of maps instead of lists in the interpretation
ppedrot
2013-06-22
*
Removing a useless location in ltac trace mechanism.
ppedrot
2013-05-30
*
Getting rid of LtacLocated exception transformer.
ppedrot
2013-05-28
*
Splitting Term into five unrelated interfaces:
ppedrot
2013-04-29
*
Revised the Ltac trace mechanism so that trace breaking due to
herbelin
2013-02-17
*
Modulification of identifier
ppedrot
2012-12-14
*
still some more dead code removal
letouzey
2012-10-06
*
Clean-up : removal of Proof_type.tactic_expr
letouzey
2012-10-06
*
Proof_type: rule now degenerates to prim_rule
letouzey
2012-10-06
*
Clean-up : no more Proof_type.proof_tree
letouzey
2012-10-06
*
Clean-up of proof_type.ml : no more Nested nor abstract_tactic_box
letouzey
2012-10-06
*
Remove some more "open" and dead code thanks to OCaml4 warnings
letouzey
2012-10-02
*
This patch removes unused "open" (automatically generated from
regisgia
2012-09-14
*
Updating headers.
herbelin
2012-08-08
*
Added an indirection with respect to Loc in Compat. As many [open Compat]
ppedrot
2012-06-22
*
Glob_term now mli-only, operations now in Glob_ops
letouzey
2012-05-29
*
Noise for nothing
pboutill
2012-03-02
*
Rename rawterm.ml into glob_term.ml
glondu
2010-12-23
*
Change of nomenclature: rawconstr -> glob_constr
glondu
2010-12-23
*
Remove open_subgoals field of proof_tree
glondu
2010-10-06
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Added support for Ltac-matching terms with variables bound in the pattern
herbelin
2010-06-06
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Here comes the commit, announced long ago, of the new tactic engine.
aspiwack
2010-04-22
*
Generic support for open terms in tactics
herbelin
2009-12-21
*
Made the interpretation levels rlevel/glevel/tlevel truly phantom
herbelin
2009-12-19
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0
herbelin
2009-06-06
*
Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"
herbelin
2009-03-16
*
commande Timeout + compaction des traces de debug_tactic
barras
2009-03-04
*
closed bug 1898: fold x in x; added a reordering primitive tactic
barras
2008-11-26
*
Évolutions diverses et variées.
herbelin
2008-08-04
*
- Propagation des evars non résolues vers les with_bindings; permet par exemple
herbelin
2007-05-20
*
Correction du bug #1315:
notin
2007-01-22
*
affichage des ... dans les scripts
barras
2006-10-16
[next]