diff options
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrelim.ml | 3 | ||||
| -rw-r--r-- | plugins/ssr/ssrvernac.mlg | 20 |
2 files changed, 2 insertions, 21 deletions
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index a0b1d784f1..7216849948 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -209,7 +209,8 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = let mind,indb = Inductive.lookup_mind_specif env (kn,i) in let tys = indb.Declarations.mind_nf_lc in let renamed_tys = - Array.mapi (fun j t -> + Array.mapi (fun j (ctx, cty) -> + let t = Term.it_mkProd_or_LetIn cty ctx in ppdebug(lazy Pp.(str "Search" ++ Printer.pr_constr_env env (project gl) t)); let t = Arguments_renaming.rename_type t (GlobRef.ConstructRef((kn,i),j+1)) in diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index 191a4e9a20..d083d34b52 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -596,26 +596,6 @@ VERNAC COMMAND EXTEND HintView CLASSIFIED AS SIDEFF Ssrview.AdaptorDb.declare k hints } END -(** Canonical Structure alias *) - -GRAMMAR EXTEND Gram - GLOBAL: gallina_ext; - - gallina_ext: - (* Canonical structure *) - [[ IDENT "Canonical"; qid = Constr.global -> - { Vernacexpr.VernacCanonical (CAst.make @@ AN qid) } - | IDENT "Canonical"; ntn = Prim.by_notation -> - { Vernacexpr.VernacCanonical (CAst.make @@ ByNotation ntn) } - | IDENT "Canonical"; qid = Constr.global; - d = G_vernac.def_body -> - { let s = coerce_reference_to_id qid in - Vernacexpr.VernacDefinition - ((Decl_kinds.NoDischarge,Decl_kinds.CanonicalStructure), - ((CAst.make (Name s)),None), d) } - ]]; -END - (** Keyword compatibility fixes. *) (* Coq v8.1 notation uses "by" and "of" quasi-keywords, i.e., reserved *) |