diff options
| author | Pierre-Marie Pédrot | 2020-02-07 18:13:25 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-02-09 16:38:14 +0100 |
| commit | b6264bb2df9b73b905af126ede49cd31abf0e7da (patch) | |
| tree | 6eddb39c2870eb12be6d6cdb5cfe15f9eaf55513 /vernac/assumptions.ml | |
| parent | 1820f40590ec358b40e3a9c444f80c5283e55292 (diff) | |
Remove the Template Check option.
Diffstat (limited to 'vernac/assumptions.ml')
| -rw-r--r-- | vernac/assumptions.ml | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index dacef1cb18..9f92eba729 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -356,8 +356,5 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t = let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in ContextObjectMap.add (Axiom (TypeInType obj, l)) Constr.mkProp accu in - if not mind.mind_typing_flags.check_template then - let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in - ContextObjectMap.add (Axiom (TemplatePolymorphic m, l)) Constr.mkProp accu - else accu + accu in GlobRef.Map_env.fold fold graph ContextObjectMap.empty |