diff options
| author | pboutill | 2012-08-05 23:13:15 +0000 |
|---|---|---|
| committer | pboutill | 2012-08-05 23:13:15 +0000 |
| commit | bead69d09207e9624f37853ce63b695fe7ff6e87 (patch) | |
| tree | 9d317f0530aac378642dbb3cb37df395313787b4 | |
| parent | 66965ce183e30c2dc18f64f6035f2d158bc9f545 (diff) | |
Dump references in reduction tactics
Patch by Adam Chilipala.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15681 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/tacinterp.ml | 17 | ||||
| -rw-r--r-- | tactics/tacinterp.mli | 1 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 1 |
3 files changed, 19 insertions, 0 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index d7ac1e66e5..e68f55095e 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -571,6 +571,22 @@ let intern_typed_pattern ist p = let intern_typed_pattern_with_occurrences ist (l,p) = (l,intern_typed_pattern ist p) +(* This seems fairly hacky, but it's the first way I've found to get proper + globalization of [unfold]. --adamc *) +let dump_glob_red_expr = function + | Unfold occs -> List.iter (fun (_, r) -> + try + Dumpglob.add_glob (loc_of_or_by_notation Libnames.loc_of_reference r) + (Smartlocate.smart_global r) + with _ -> ()) occs + | Cbv grf | Lazy grf -> + List.iter (fun r -> + try + Dumpglob.add_glob (loc_of_or_by_notation Libnames.loc_of_reference r) + (Smartlocate.smart_global r) + with _ -> ()) grf.rConst + | _ -> () + let intern_red_expr ist = function | Unfold l -> Unfold (List.map (intern_unfold ist) l) | Fold l -> Fold (List.map (intern_constr ist) l) @@ -771,6 +787,7 @@ let rec intern_atomic lf ist x = (* Conversion *) | TacReduce (r,cl) -> + dump_glob_red_expr r; TacReduce (intern_red_expr ist r, clause_app (intern_hyp_location ist) cl) | TacChange (None,c,cl) -> TacChange (None, diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index 7ce0d3f842..b600fb5cd8 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -123,6 +123,7 @@ val interp_ltac_constr : interp_sign -> goal sigma -> glob_tactic_expr -> Evd.evar_map * constr (** Interprets redexp arguments *) +val dump_glob_red_expr : raw_red_expr -> unit val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> Evd.evar_map * red_expr (** Interprets tactic expressions *) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 46fdeb5326..a4a14b7b30 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1317,6 +1317,7 @@ let vernac_check_may_eval redexp glopt rc = | None -> msg_notice (print_judgment env j) | Some r -> + Tacinterp.dump_glob_red_expr r; let (sigma',r_interp) = interp_redexp env sigma' r in let redfun = fst (reduction_of_red_expr r_interp) in msg_notice (print_eval redfun env sigma' rc j) |