];
END
+(* TODO a lot of hard coded URIs, move them in HelmLibraryObjects *)
+
let _ =
+ (* TODO cut-and-pasted code: here, in arit_notation.ml and
+ * disambiguateChoices.ml *)
+ let uri s = UriManager.uri_of_string s in
+ let const s = Cic.Const (uri s, []) in
+ let mutind s = Cic.MutInd (uri s, 0, []) in
DisambiguateChoices.add_symbol_choice "eq"
("leibnitz's equality",
(fun interp _ args ->
Cic.Appl [
Cic.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []);
Cic.Implicit (Some `Type); t1; t2
- ]))
+ ]));
+ DisambiguateChoices.add_symbol_choice "eq"
+ ("equality over objects with sort Type",
+ (fun interp _ args ->
+ let t1, t2 =
+ match args with
+ | [t1; t2] -> t1, t2
+ | _ -> raise DisambiguateChoices.Invalid_choice
+ in
+ Cic.Appl [
+ Cic.MutInd (HelmLibraryObjects.Logic_Type.eqt_URI, 0, []);
+ Cic.Implicit (Some `Type); t1; t2
+ ]));
+ DisambiguateChoices.add_binary_op "and" "logical and"
+ (mutind "cic:/Coq/Init/Logic/and.ind");
+ DisambiguateChoices.add_binary_op "or" "logical or"
+ (mutind "cic:/Coq/Init/Logic/or.ind");
+ DisambiguateChoices.add_unary_op "not" "logical not"
+ (const "cic:/Coq/Init/Logic/not.con");