diff options
| author | msozeau | 2011-04-13 14:26:59 +0000 |
|---|---|---|
| committer | msozeau | 2011-04-13 14:26:59 +0000 |
| commit | d98dfbcae463f8d699765e2d7004becd7714d6cf (patch) | |
| tree | 976e3e3ae284485cabd567d7c3504bc7b8817554 /plugins/subtac/subtac.ml | |
| parent | 5113afbb6e8c1f9122b37c37b0561c529c406256 (diff) | |
Add [Polymorphic] flag for defs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13988 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/subtac/subtac.ml')
| -rw-r--r-- | plugins/subtac/subtac.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml index fbdaa8d3b1..7faf780330 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 = fst kind = Global in + let global = pi1 kind = Global in List.iter (fun (is_coe,(idl,c)) -> if Dumpglob.dump () then List.iter (fun lid -> @@ -137,7 +137,8 @@ let subtac (loc, command) = Dumpglob.dump_definition lid false "def"; (match expr with | ProveBody (bl, t) -> - start_proof_and_print env isevars (Some lid) (Global, DefinitionBody Definition) (bl,t) + start_proof_and_print env isevars (Some lid) + (pi1 defkind, pi2 defkind, DefinitionBody Definition) (bl,t) (fun _ _ -> ()) | DefineBody (bl, _, c, tycon) -> ignore(Subtac_pretyping.subtac_proof defkind hook env isevars id bl c tycon)) @@ -148,7 +149,7 @@ let subtac (loc, command) = let _ = trace (str "Building fixpoint") in ignore(Subtac_command.build_recursive l) - | VernacStartTheoremProof (thkind, [Some id, (bl,t,guard)], lettop, hook) -> + | VernacStartTheoremProof (thkind, p, [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"; @@ -160,12 +161,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, Proof thkind) (bl,t) hook + start_proof_and_print env isevars (Some id) (Global, p, Proof thkind) (bl,t) hook | VernacAssumption (stre,nl,l) -> vernac_assumption env isevars stre l nl - | VernacInstance (abst, glob, sup, is, props, pri) -> + | VernacInstance (abst, glob, poly, sup, is, props, pri) -> dump_constraint "inst" is; if abst then error "Declare Instance not supported here."; |