exception BaseUriNotSetYet
-type tactic =
- (NotationPt.term, NotationPt.term,
- NotationPt.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, _ ->
| false -> NCic.Implicit `Term)
~mk_appl:(function
(NCic.Appl l)::tl -> NCic.Appl (l@tl) | l -> NCic.Appl l)
- ~term_of_uri:(fun _ -> assert false)
~term_of_nref:(fun nref -> NCic.Const nref)
name dsc
| LexiconAst.Number_alias (_, dsc) ->
let estatus = LexiconEngine.set_proof_aliases estatus diff in
estatus, cic
;;
-let disambiguate_command estatus ?baseuri (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, GrafiteAst.Select(loc,uri)
- | 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,cmd
- | GrafiteAst.Obj (loc,obj) -> (* MATITA 1.0 *) assert false
- | GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans) -> (* MATITA 1.0 *) assert false