exception BaseUriNotSetYet
-type tactic =
- (CicNotationPt.term, CicNotationPt.term,
- CicNotationPt.term GrafiteAst.reduction, string)
- GrafiteAst.tactic
-
-type lazy_tactic =
- (Cic.term, Cic.lazy_term, Cic.lazy_term GrafiteAst.reduction, string)
- GrafiteAst.tactic
-
let singleton msg = function
| [x], _ -> x
| l, _ ->
| LexiconAst.Ident_alias (name, uri) ->
uri, `Sym_interp
(fun l->assert(l = []);
- try
- let nref = NReference.reference_of_string uri in
- NCic.Const nref
- with
- NReference.IllFormedReference _ ->
- let uri = UriManager.uri_of_string uri in
- fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)))
+ let nref = NReference.reference_of_string uri in
+ NCic.Const nref)
;;
type pattern =
- CicNotationPt.term Disambiguate.disambiguator_input option *
+ NotationPt.term Disambiguate.disambiguator_input option *
(string * NCic.term) list * NCic.term option
let disambiguate_npattern (text, prefix_len, (wanted, hyp_paths, goal_path)) =
in
let name =
match obj with
- | CicNotationPt.Inductive (_,(name,_,_,_)::_)
- | CicNotationPt.Record (_,name,_,_) -> name ^ ".ind"
- | CicNotationPt.Theorem (_,name,_,_,_) -> name ^ ".con"
- | CicNotationPt.Inductive _ -> assert false
+ | NotationPt.Inductive (_,(name,_,_,_)::_)
+ | NotationPt.Record (_,name,_,_) -> name ^ ".ind"
+ | NotationPt.Theorem (_,name,_,_,_) -> name ^ ".con"
+ | NotationPt.Inductive _ -> assert false
in
- UriManager.uri_of_string (baseuri ^ "/" ^ name)
+ NUri.uri_of_string (baseuri ^ "/" ^ name)
in
let diff, _, _, cic =
singleton "third"
~description_of_alias:LexiconAst.description_of_alias
~mk_choice:ncic_mk_choice
~mk_implicit ~fix_instance
- ~uri:(OCic2NCic.nuri_of_ouri uri)
+ ~uri
~rdb:estatus
~aliases:estatus#lstatus.LexiconEngine.aliases
~universe:(Some estatus#lstatus.LexiconEngine.multi_aliases)
let estatus = LexiconEngine.set_proof_aliases estatus diff in
estatus, cic
;;
-let disambiguate_command estatus ?baseuri metasenv (text,prefix_len,cmd)=
+
+let disambiguate_command estatus (text,prefix_len,cmd)=
match cmd with
- | GrafiteAst.Index(loc,key,uri) -> (* MATITA 1.0 *) assert false
- | GrafiteAst.Select (loc,uri) ->
- estatus, metasenv, GrafiteAst.Select(loc,uri)
- | GrafiteAst.Pump(loc,i) ->
- estatus, metasenv, GrafiteAst.Pump(loc,i)
- | GrafiteAst.PreferCoercion (loc,t) -> (* MATITA 1.0 *) assert false
- | GrafiteAst.Coercion (loc,t,b,a,s) -> (* MATITA 1.0 *) assert false
- | GrafiteAst.Inverter (loc,n,indty,params) -> (* MATITA 1.0 *) assert false
- | GrafiteAst.Default _
- | GrafiteAst.Drop _
| GrafiteAst.Include _
| GrafiteAst.Print _
- | GrafiteAst.Qed _
| GrafiteAst.Set _ as cmd ->
- estatus,metasenv,cmd
- | GrafiteAst.Obj (loc,obj) -> (* MATITA 1.0 *) assert false
- | GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans) -> (* MATITA 1.0 *) assert false
+ estatus,cmd