argument->term uses elaborate (caveat, one may expect a type)

math-comp · Aug 14, 2020 · 67342d7 · 67342d7
1 parent 77862d8
commit 67342d7
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/hb.elpi b/hb.elpi
@@ -123,7 +123,7 @@ argument->gref X _ :- coq.error "Argument" X "is expected to be a string".
 
 pred argument->term i:argument, o:term.
 argument->term (str S) (global GR) :- !, argument->gref (str S) GR.
-argument->term (trm T) T :- !, std.assert-ok! (coq.typecheck T _) "not well typed term".
+argument->term (trm T) T1 :- !, std.assert-ok! (coq.elaborate-skeleton T _ T1) "not well typed term".
 argument->term X _ :- coq.error "Argument" X " is expected to be a term or a string".
 
 % Type to share code between HB.mixin and HB.factory (that supports alias factories)