diff options
| author | msozeau | 2011-04-13 14:29:02 +0000 |
|---|---|---|
| committer | msozeau | 2011-04-13 14:29:02 +0000 |
| commit | 60bc3cbe72083f4fa1aa759914936e4fa3d6b42e (patch) | |
| tree | 0eeffe9b7b098ad653ffeb6ad963c62223245d0e /plugins/subtac/subtac.ml | |
| parent | 3b11686e4f78f6d166f84d990ac4fedb4d3e800a (diff) | |
Revert "Add [Polymorphic] flag for defs"
This reverts commit 33434695615806a85cec88452c93ea69ffc0e719.
Conflicts:
kernel/term_typing.ml
test-suite/success/polymorphism.v
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13998 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/subtac/subtac.ml')
| -rw-r--r-- | plugins/subtac/subtac.ml | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml index 7faf780330..fbdaa8d3b1 100644 --- a/plugins/subtac/subtac.ml +++ b/plugins/subtac/subtac.ml @@ -113,7 +113,7 @@ let dump_constraint ty ((loc, n), _, _) = let dump_variable lid = () let vernac_assumption env isevars kind l nl = - let global = pi1 kind = Global in + let global = fst kind = Global in List.iter (fun (is_coe,(idl,c)) -> if Dumpglob.dump () then List.iter (fun lid -> @@ -137,8 +137,7 @@ let subtac (loc, command) = Dumpglob.dump_definition lid false "def"; (match expr with | ProveBody (bl, t) -> - start_proof_and_print env isevars (Some lid) - (pi1 defkind, pi2 defkind, DefinitionBody Definition) (bl,t) + start_proof_and_print env isevars (Some lid) (Global, DefinitionBody Definition) (bl,t) (fun _ _ -> ()) | DefineBody (bl, _, c, tycon) -> ignore(Subtac_pretyping.subtac_proof defkind hook env isevars id bl c tycon)) @@ -149,7 +148,7 @@ let subtac (loc, command) = let _ = trace (str "Building fixpoint") in ignore(Subtac_command.build_recursive l) - | VernacStartTheoremProof (thkind, p, [Some id, (bl,t,guard)], lettop, hook) -> + | VernacStartTheoremProof (thkind, [Some id, (bl,t,guard)], lettop, hook) -> if guard <> None then error "Do not support building theorems as a fixpoint."; Dumpglob.dump_definition id false "prf"; @@ -161,12 +160,12 @@ let subtac (loc, command) = errorlabstrm "Subtac_command.StartProof" (str "Proof editing mode not supported in module types"); check_fresh id; - start_proof_and_print env isevars (Some id) (Global, p, Proof thkind) (bl,t) hook + start_proof_and_print env isevars (Some id) (Global, Proof thkind) (bl,t) hook | VernacAssumption (stre,nl,l) -> vernac_assumption env isevars stre l nl - | VernacInstance (abst, glob, poly, sup, is, props, pri) -> + | VernacInstance (abst, glob, sup, is, props, pri) -> dump_constraint "inst" is; if abst then error "Declare Instance not supported here."; |