gmalecha / template-coq

Reflection library for Coq
MIT License
12 stars 0 forks source link

template-coq does not build with Coq master #44

Closed JasonGross closed 6 years ago

JasonGross commented 6 years ago

tail end of the build is:

Vernac entry "Make_vernac" misses a classifier. A classifier is a function that returns an expression of type vernac_classification (see Vernacexpr). You can: - Use '... EXTEND Make_vernac CLASSIFIED AS QUERY ...' if the new vernacular command does not alter the system state;
- Use '... EXTEND Make_vernac CLASSIFIED AS SIDEFF ...' if the new vernacular command alters the system state but not the parser nor it starts a proof or ends one;
- Use '... EXTEND Make_vernac CLASSIFIED BY f ...' to specify a global function f.  The function f will be called passing "Make_vernac" as the only argument;
- Add a specific classifier in each clause using the syntax:
'[...] => [ f ] -> [...]'.
Specific classifiers have precedence over global classifiers. Only one classifier is called.

Vernac entry "Make_recursive" misses a classifier. A classifier is a function that returns an expression of type vernac_classification (see Vernacexpr). You can: - Use '... EXTEND Make_recursive CLASSIFIED AS QUERY ...' if the new vernacular command does not alter the system state;
- Use '... EXTEND Make_recursive CLASSIFIED AS SIDEFF ...' if the new vernacular command alters the system state but not the parser nor it starts a proof or ends one;
- Use '... EXTEND Make_recursive CLASSIFIED BY f ...' to specify a global function f.  The function f will be called passing "Make_recursive" as the only argument;
- Add a specific classifier in each clause using the syntax:
'[...] => [ f ] -> [...]'.
Specific classifiers have precedence over global classifiers. Only one classifier is called.

Vernac entry "Make_recursive_hnf" misses a classifier. A classifier is a function that returns an expression of type vernac_classification (see Vernacexpr). You can: - Use '... EXTEND Make_recursive_hnf CLASSIFIED AS QUERY ...' if the new vernacular command does not alter the system state;
- Use '... EXTEND Make_recursive_hnf CLASSIFIED AS SIDEFF ...' if the new vernacular command alters the system state but not the parser nor it starts a proof or ends one;
- Use '... EXTEND Make_recursive_hnf CLASSIFIED BY f ...' to specify a global function f.  The function f will be called passing "Make_recursive_hnf" as the only argument;
- Add a specific classifier in each clause using the syntax:
'[...] => [ f ] -> [...]'.
Specific classifiers have precedence over global classifiers. Only one classifier is called.

Vernac entry "Unquote_vernac" misses a classifier. A classifier is a function that returns an expression of type vernac_classification (see Vernacexpr). You can: - Use '... EXTEND Unquote_vernac CLASSIFIED AS QUERY ...' if the new vernacular command does not alter the system state;
- Use '... EXTEND Unquote_vernac CLASSIFIED AS SIDEFF ...' if the new vernacular command alters the system state but not the parser nor it starts a proof or ends one;
- Use '... EXTEND Unquote_vernac CLASSIFIED BY f ...' to specify a global function f.  The function f will be called passing "Unquote_vernac" as the only argument;
- Add a specific classifier in each clause using the syntax:
'[...] => [ f ] -> [...]'.
Specific classifiers have precedence over global classifiers. Only one classifier is called.

Vernac entry "Make_tests" misses a classifier. A classifier is a function that returns an expression of type vernac_classification (see Vernacexpr). You can: - Use '... EXTEND Make_tests CLASSIFIED AS QUERY ...' if the new vernacular command does not alter the system state;
- Use '... EXTEND Make_tests CLASSIFIED AS SIDEFF ...' if the new vernacular command alters the system state but not the parser nor it starts a proof or ends one;
- Use '... EXTEND Make_tests CLASSIFIED BY f ...' to specify a global function f.  The function f will be called passing "Make_tests" as the only argument;
- Add a specific classifier in each clause using the syntax:
'[...] => [ f ] -> [...]'.
Specific classifiers have precedence over global classifiers. Only one classifier is called.

File "src/reify.ml4", line 37, characters 4-29:
Error: Unbound value Libnames.constr_of_global
Makefile.coq:579: recipe for target 'src/reify.cmx' failed
gmalecha commented 6 years ago

The development has moved to https://github.com/Template-Coq/template-coq

JasonGross commented 6 years ago

You might want to contact GitHub support and have them make that repo the base one that all others are forked from

mattam82 commented 6 years ago

I will. Le sam. 9 déc. 2017 à 05:08, Jason Gross notifications@github.com a écrit :

You might want to contact GitHub support and have them make that repo the base one that all others are forked from

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/gmalecha/template-coq/issues/44#issuecomment-350424588, or mute the thread https://github.com/notifications/unsubscribe-auth/AAGARbKuw6UjHph-QtrKoBnyr7T0Y1Xyks5s-hXBgaJpZM4Q7eau .