From e4888cba796e8255ae768e85ca27454ea4142ea3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 12 Nov 2008 12:41:23 +0000 Subject: [PATCH] some new exports --- helm/software/components/cic_disambiguation/disambiguate.ml | 2 ++ helm/software/components/cic_disambiguation/disambiguate.mli | 3 +++ 2 files changed, 5 insertions(+) diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml index e11927d7d..9effb6ae4 100644 --- a/helm/software/components/cic_disambiguation/disambiguate.ml +++ b/helm/software/components/cic_disambiguation/disambiguate.ml @@ -895,6 +895,8 @@ let domain_of_obj ~context ast = let domain_of_obj ~context obj = uniq_domain (domain_of_obj ~context obj) +let domain_of_ast_term = domain_of_term;; + let domain_of_term ~context term = let context = List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context diff --git a/helm/software/components/cic_disambiguation/disambiguate.mli b/helm/software/components/cic_disambiguation/disambiguate.mli index 99c1e4556..78fe41768 100644 --- a/helm/software/components/cic_disambiguation/disambiguate.mli +++ b/helm/software/components/cic_disambiguation/disambiguate.mli @@ -52,6 +52,9 @@ type ('a,'m) test_result = | Ok of 'a * 'm | Ko of Stdpp.location option * string Lazy.t | Uncertain of Stdpp.location option * string Lazy.t +exception Try_again of string Lazy.t + +val domain_of_ast_term: context:Cic.name list -> CicNotationPt.term -> domain module type Disambiguator = sig -- 2.39.2