diff options
| author | letouzey | 2012-05-29 11:08:44 +0000 |
|---|---|---|
| committer | letouzey | 2012-05-29 11:08:44 +0000 |
| commit | a936f2e879ac1f9b2e7e9d8a5376469e3d53c606 (patch) | |
| tree | 7f0972729eb41828ad9abbaf0dc61ce2366ef870 /tactics | |
| parent | b31b48407a9f5d36cefd6dec3ddf3e0b8391f14c (diff) | |
Glob_term now mli-only, operations now in Glob_ops
Stuff about reductions now in genredexpr.mli, operations in redops.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15374 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.ml | 2 | ||||
| -rw-r--r-- | tactics/eauto.ml4 | 2 | ||||
| -rw-r--r-- | tactics/elim.ml | 1 | ||||
| -rw-r--r-- | tactics/extratactics.ml4 | 1 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 4 | ||||
| -rw-r--r-- | tactics/tactics.ml | 2 |
6 files changed, 8 insertions, 4 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 6e338c4cbb..f167a91a30 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -26,7 +26,7 @@ open Matching open Tacmach open Proof_type open Pfedit -open Glob_term +open Genredexpr open Evar_refiner open Tacred open Tactics diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 8b773762f0..e9602762d2 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -26,7 +26,7 @@ open Tactics open Pattern open Clenv open Auto -open Glob_term +open Genredexpr open Hiddentac open Tacexpr open Misctypes diff --git a/tactics/elim.ml b/tactics/elim.ml index bd304d9753..de55128430 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -25,6 +25,7 @@ open Tactics open Hiddentac open Genarg open Tacexpr +open Misctypes let introElimAssumsThen tac ba = let nassums = diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index a2d1caf5f8..a74bdad29b 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -16,6 +16,7 @@ open Mod_subst open Names open Tacexpr open Glob_term +open Glob_ops open Tactics open Errors open Util diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index f3b6c58c0e..8e68d8e705 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -15,7 +15,9 @@ open Libobject open Pattern open Matching open Pp +open Genredexpr open Glob_term +open Glob_ops open Sign open Tacred open Errors @@ -172,7 +174,7 @@ let _ = [ "red", TacReduce(Red false,nocl); "hnf", TacReduce(Hnf,nocl); "simpl", TacReduce(Simpl None,nocl); - "compute", TacReduce(Cbv all_flags,nocl); + "compute", TacReduce(Cbv Redops.all_flags,nocl); "intro", TacIntroMove(None,MoveLast); "intros", TacIntroPattern []; "assumption", TacAssumption; diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 897e1d7ef2..ab4b08e7da 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -25,7 +25,7 @@ open Libnames open Evd open Pfedit open Tacred -open Glob_term +open Genredexpr open Tacmach open Proof_type open Logic |