diff options
| author | Maxime Dénès | 2017-10-25 10:16:57 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-10-25 10:16:57 +0200 |
| commit | ad973248998da8d7d10ed00f4bcd6f383ba9a171 (patch) | |
| tree | 705a2b2de824b39d97a28fcea3b8287b53204b54 /vernac | |
| parent | 7d2dfd6fabd5d447166b1cb0e3b2993cc8abf4b3 (diff) | |
| parent | 069ab52e2af900d498395ebd1b00b7983152326e (diff) | |
Merge PR #6009: Master+misc typos dead code etc
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/record.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/vernac/record.ml b/vernac/record.ml index 9a8657c3c3..5533fe5b38 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -418,7 +418,6 @@ let declare_structure finite univs id idbuild paramimpls params arity template begin let env = Global.env () in let env' = Environ.push_context ctx env in - (* let env'' = Environ.push_rel_context params env' in *) let evd = Evd.from_env env' in Inductiveops.infer_inductive_subtyping env' evd mie end |