diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-11-29 19:05:53 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-11-29 19:13:30 +0100 |
| commit | e98d3c3793f26265a49f63a6e78d704f88341df9 (patch) | |
| tree | c0328afc0034f3262dca2ca067531ee19bbb0ee0 /toplevel | |
| parent | 103ec7205d9038f1f3821f9287e3bb0907a1e3ec (diff) | |
| parent | 8d6e58e16cc53a3198eb4c4afef0a2c39f6a5c56 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/command.ml | 6 | ||||
| -rw-r--r-- | toplevel/obligations.ml | 4 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 6 |
3 files changed, 10 insertions, 6 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 0b709a3fc..91cfddb54 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -1128,7 +1128,8 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind if List.exists Option.is_empty fixdefs then (* Some bodies to define by proof *) let thms = - List.map3 (fun id t (len,imps,_) -> (id,(t,(len,imps)))) fixnames fixtypes fiximps in + List.map3 (fun id t (len,imps,_) -> ((id,pl),(t,(len,imps)))) + fixnames fixtypes fiximps in let init_tac = Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC) fixdefs) in @@ -1164,7 +1165,8 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n if List.exists Option.is_empty fixdefs then (* Some bodies to define by proof *) let thms = - List.map3 (fun id t (len,imps,_) -> (id,(t,(len,imps)))) fixnames fixtypes fiximps in + List.map3 (fun id t (len,imps,_) -> ((id,pl),(t,(len,imps)))) + fixnames fixtypes fiximps in let init_tac = Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC) fixdefs) in diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index e34cbab5f..50ecef0b0 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -826,10 +826,10 @@ let obligation_terminator name num guard hook pf = Inductiveops.control_only_guard (Global.env ()) body; (** Declare the obligation ourselves and drop the hook *) let prg = get_info (ProgMap.find name !from_prg) in - let prg = { prg with prg_ctx = uctx } in + let prg = { prg with prg_ctx = fst uctx } in let obls, rem = prg.prg_obligations in let obl = obls.(num) in - let ctx = Evd.evar_context_universe_context uctx in + let ctx = Evd.evar_context_universe_context (fst uctx) in let (_, obl) = declare_obligation prg obl body ty ctx in let obls = Array.copy obls in let _ = obls.(num) <- obl in diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index b6a4ab93e..b3512ffde 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -2048,7 +2048,7 @@ let check_vernac_supports_polymorphism c p = let enforce_polymorphism = function | None -> Flags.is_universe_polymorphism () - | Some b -> b + | Some b -> Flags.make_polymorphic_flag b; b (** A global default timeout, controled by option "Set Default Timeout n". Use "Unset Default Timeout" to deactivate it (or set it to 0). *) @@ -2149,7 +2149,8 @@ let interp ?(verbosely=true) ?proof (loc,c) = then Flags.verbosely (interp ?proof ~loc locality poly) c else Flags.silently (interp ?proof ~loc locality poly) c; if orig_program_mode || not !Flags.program_mode || isprogcmd then - Flags.program_mode := orig_program_mode + Flags.program_mode := orig_program_mode; + ignore (Flags.use_polymorphic_flag ()) end with | reraise when @@ -2161,6 +2162,7 @@ let interp ?(verbosely=true) ?proof (loc,c) = let e = locate_if_not_already loc e in let () = restore_timeout () in Flags.program_mode := orig_program_mode; + ignore (Flags.use_polymorphic_flag ()); iraise e and aux_list ?locality ?polymorphism isprogcmd l = List.iter (aux false) (List.map snd l) |