diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-11-20 20:33:27 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-11-20 20:33:27 +0100 |
| commit | 12c61c7ab522ea58bf8c5692de7130e124a2cc0a (patch) | |
| tree | 6a58fba73892d1f300c058326ff069e938fccf10 /toplevel/obligations.ml | |
| parent | 579770c44251f2b8d01ecc6252810ec80da374f5 (diff) | |
Exporting the function handling side-effects only applied to terms.
Diffstat (limited to 'toplevel/obligations.ml')
| -rw-r--r-- | toplevel/obligations.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 38580882e..be5711820 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -780,7 +780,7 @@ let solve_by_tac name evi t poly ctx = let (entry,_,ctx') = Pfedit.build_constant_by_tactic id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps concl (Tacticals.New.tclCOMPLETE t) in let env = Global.env () in - let entry = Term_typing.handle_side_effects env entry in + let entry = Term_typing.handle_entry_side_effects env entry in let body, eff = Future.force entry.Entries.const_entry_body in assert(Declareops.side_effects_is_empty eff); assert(Univ.ContextSet.is_empty (snd body)); |